let I be non empty set ; :: thesis: for F, G being Group-Family of I
for x, y being Function st ( for i being Element of I 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 Element of I 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 Element of I 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 Element of I 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 Element of I st i in support (y,G) holds
i in support (x,F)

proof

let i be Element of I; :: 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)
consider hi being Homomorphism of (F . i),(G . i) such that
A3: y . i = hi . (x . i) by A1;
ex Z being Group st
( Z = G . i & hi . (x . i) <> 1_ Z & i in I ) by A2, A3, Def1;
then x . i <> 1_ (F . i) by GROUP_6:31;
hence i in support (x,F) by Def1; :: thesis: verum

end;

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