let I be non empty set ; 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; 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; ( ( 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)
; 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)
hence
support (y,G) c= support (x,F)
; verum