let I be non empty set ; :: thesis: for F, G being Group-Family of I
for x, y being Function st ( for i being object st i in I holds
ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) holds
support (y,G) c= support (x,F)
let F, G be Group-Family of I; :: thesis: for x, y being Function st ( for i being object st i in I holds
ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) holds
support (y,G) c= support (x,F)
let x, y be Function; :: thesis: ( ( for i being object st i in I holds
ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) implies support (y,G) c= support (x,F) )
assume A1: for i being object st i in I holds
ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ; :: thesis: support (y,G) c= support (x,F)
for i being object st i in support (y,G) holds
i in support (x,F)

proof

let i be object ; :: thesis: ( i in support (y,G) implies i in support (x,F) )
assume A2: i in support (y,G) ; :: thesis: i in support (x,F)
then consider hi being Homomorphism of (F . i),(G . i) such that
A3: y . i = hi . (x . i) by A1;
hi . (x . i) <> 1_ (G . i) by A2, A3, Def1;
then x . i <> 1_ (F . i) by GROUP_6:31;
hence i in support (x,F) by A2, Def1; :: thesis: verum

end;

hence support (y,G) c= support (x,F) ; :: thesis: verum