I am building up a system which contains both Family of sets and function, and I’m facing lots of errors that goes:

"The term "_" has type "_" while it is expected to have type "_"."

Here are my codes:

From mathcomp
 Require Import ssreflect.
 Require Import Ensembles.
 Require Import Classical.



Ltac RAA := apply NNPP; intro.
Ltac Subset := unfold Included; intros. 
Ltac Seteq:= apply Extensionality_Ensembles; unfold Same_set;split.


Notation "x ∈ A" := (In _ A x)(at level 50, no associativity).
Notation "A ⊆ B" := (Included _ A B)(at level 100, no associativity).
Notation "A ∩ B" := (Intersection _ A B)(at level 80, no associativity).
Notation "A ∪ B" := (Union _ A B)(at level 80, no associativity).
Notation "A  B" := (Setminus _ A B)(at level 60, no associativity).
Notation "∅":= (Empty_set _).
Notation Ω:= (Full_set _).

Section Sets.
Variable U:Type.
Definition Ensemble := U -> Prop.
Definition In (A:Ensemble) (x:U) : Prop := A x.

Inductive Singleton (x:U) : Ensemble := In_singleton : In (Singleton x) x.

End Sets.

Section Family.

Variable U:Type.
Notation set := (Ensemble U).
Variable I: Type.
Definition Fam:= I ->set.
Definition UFam (F:Fam)(X:set):Fam:=fun i:I=> X∪(F i).
Definition IFam (F:Fam)(X:set):Fam:=fun i:I=> X∩(F i).
Inductive UnionF (X:Fam):set:=
unionf_intro:forall x:U, (exists i:I,(x∈(X i)))->(x∈UnionF X).

Inductive InterF (X:Fam):set:=
interf_intro:forall x:U, (forall i:I,(x∈(X i)))->(x∈InterF X).

End Family.

Section Function.
Variables U V:Type.

Notation set := (Ensemble U).
Notation Domain := (Ensemble U).
Notation Range := (Ensemble V).


Inductive Im (X:Domain)(f:U->V) : Range := 
Im_intro : forall x:U, x∈X->(f x)∈(Im X f).

Inductive InvIm (Y:Range)(f:U->V) : Domain := 
InvIm_intro : forall x:U, (f x)∈Y->x∈(InvIm Y f).

End Function.

Section HW_9_E1.

Variables U V:Type.

Lemma E1_1:forall (X Y:Fam)(i:I)(f:U->V)(x:U)(y:V),
(Im (UnionF X) f) = Union (Im (X i) f).

There’s an error in the Lemma:

Lemma E1_1:forall (X Y:Fam)(i:I)(f:U->V)(x:U)(y:V),(Im (UnionF X) f) = Union (Im (X i) f).

Say, for example, how can I write the Lemma:

forall f:U->V, (X_{i}){iin I}subseteq U and (Y{i})_{iin I}subseteq Y,

f[bigcup_{iin I}X_{i}] = bigcup_{iin I} f[X_{i}]

What occurs the error and how could I solve it?