let I be non empty set ; :: thesis: for A, B being Group-Family of I
for f being ManySortedSet of I holds
( f is Homomorphism-Family of A,B iff for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) )
let A, B be Group-Family of I; :: thesis: for f being ManySortedSet of I holds
( f is Homomorphism-Family of A,B iff for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) )
let f be ManySortedSet of I; :: thesis: ( f is Homomorphism-Family of A,B iff for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) )
thus ( f is Homomorphism-Family of A,B implies for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) ) :: thesis: ( ( for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) ) implies f is Homomorphism-Family of A,B )

proof

assume A1: f is Homomorphism-Family of A,B ; :: thesis: for i being Element of I holds f . i is Homomorphism of (A . i),(B . i)
let i be Element of I; :: thesis: f . i is Homomorphism of (A . i),(B . i)
reconsider ff = f as Homomorphism-Family of A,B by A1;
( ff . i = f . i & ff . i is Homomorphism of (A . i),(B . i) ) ;
hence f . i is Homomorphism of (A . i),(B . i) ; :: thesis: verum

end;

thus ( ( for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) ) implies f is Homomorphism-Family of A,B ) :: thesis: verum

proof

assume A1: for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) ; :: thesis: f is Homomorphism-Family of A,B
for i being object st i in I holds
f . i is Function of ((Carrier A) . i),((Carrier B) . i)

proof

let i be object ; :: thesis: ( i in I implies f . i is Function of ((Carrier A) . i),((Carrier B) . i) )
assume i in I ; :: thesis: f . i is Function of ((Carrier A) . i),((Carrier B) . i)
then reconsider ii = i as Element of I ;
( (Carrier A) . i = the carrier of (A . ii) & (Carrier B) . i = the carrier of (B . ii) ) by Th9;
hence f . i is Function of ((Carrier A) . i),((Carrier B) . i) by A1; :: thesis: verum

end;

then f is ManySortedFunction of Carrier A, Carrier B by PBOOLE:def 15;
hence f is Homomorphism-Family of A,B by A1, Def11; :: thesis: verum

end;