let I be non empty set ; :: thesis: for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds
product F1 is Subgroup of product F2
let F1, F2 be Group-Family of I; :: thesis: ( ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) implies product F1 is Subgroup of product F2 )
assume A1: for i being Element of I holds F1 . i is Subgroup of F2 . i ; :: thesis: product F1 is Subgroup of product F2
deffunc H₁( Element of I) -> Element of bool [: the carrier of (product F1), the carrier of (F2 . $1):] = (incl ((F1 . $1),(F2 . $1))) * (proj (F1,$1));
A2: for i being Element of I holds H₁(i) is Homomorphism of (product F1),(F2 . i) ;
consider f being Homomorphism-Family of product F1,F2 such that
A3: for i being Element of I holds f . i = H₁(i) from GROUP_23:sch 5(A2);
A4: for g being Element of (product F1)
for i being Element of I holds (f . i) . g = g . i

proof

let g be Element of (product F1); :: thesis: for i being Element of I holds (f . i) . g = g . i
let i be Element of I; :: thesis: (f . i) . g = g . i
B1: F1 . i is Subgroup of F2 . i by A1;
(proj (F1,i)) . g in F1 . i ;
then g . i is Element of (F1 . i) by Def13;
then B2: (incl ((F1 . i),(F2 . i))) . (g . i) = g . i by B1, Th18;
(f . i) . g = ((incl ((F1 . i),(F2 . i))) * (proj (F1,i))) . g by A3
.= (incl ((F1 . i),(F2 . i))) . ((proj (F1,i)) . g) by FUNCT_2:15
.= g . i by B2, Def13 ;
hence (f . i) . g = g . i ; :: thesis: verum

end;

consider phi being Homomorphism of (product F1),(product F2) such that
A5: for g being Element of (product F1)
for i being Element of I holds (f . i) . g = (proj (F2,i)) . (phi . g) by Th39;
for g being Element of (product F1) holds phi . g = g

proof

let g be Element of (product F1); :: thesis: phi . g = g
B1: for i being object st i in I holds
(phi . g) . i = g . i

proof

let i be object ; :: thesis: ( i in I implies (phi . g) . i = g . i )
assume i in I ; :: thesis: (phi . g) . i = g . i
then reconsider j = i as Element of I ;
g . j = (f . j) . g by A4
.= (proj (F2,j)) . (phi . g) by A5
.= (phi . g) . j by Def13 ;
hence (phi . g) . i = g . i ; :: thesis: verum

end;

dom g = I by GROUP_19:3;
hence g = phi . g by B1, GROUP_19:3; :: thesis: verum

end;

hence product F1 is Subgroup of product F2 by InclByAnyOtherName; :: thesis: verum