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
A2: for x being object st x in [#] (product F1) holds
x in [#] (product F2)

proof

let x be object ; :: thesis: ( x in [#] (product F1) implies x in [#] (product F2) )
assume x in [#] (product F1) ; :: thesis: x in [#] (product F2)
then reconsider x = x as Element of (product F1) ;
A3: dom x = I by GROUP_19:3;
reconsider z = Carrier F2 as ManySortedSet of I ;
A4: dom z = I by PARTFUN1:def 2;
for i being object st i in I holds
x . i in z . i

proof

let i be object ; :: thesis: ( i in I implies x . i in z . i )
assume i in I ; :: thesis: x . i in z . i
then reconsider i = i as Element of I ;
A5: z . i = [#] (F2 . i) by PENCIL_3:7;
x in product F1 ;
then A6: x . i in F1 . i by GROUP_19:5;
F1 . i is Subgroup of F2 . i by A1;
then [#] (F1 . i) c= [#] (F2 . i) by GROUP_2:def 5;
hence x . i in z . i by A5, A6; :: thesis: verum

end;

then x in product z by A3, A4, CARD_3:def 5;
hence x in [#] (product F2) by GROUP_7:def 2; :: thesis: verum

end;

then A7: [#] (product F1) c= [#] (product F2) ;
then [:([#] (product F1)),([#] (product F1)):] c= [:([#] (product F2)),([#] (product F2)):] by ZFMISC_1:96;
then reconsider f2 = the multF of (product F2) || ([#] (product F1)) as Function of [:([#] (product F1)),([#] (product F1)):],([#] (product F2)) by FUNCT_2:32;
reconsider f1 = the multF of (product F1) as Function of [:([#] (product F1)),([#] (product F1)):],([#] (product F2)) by A7, FUNCT_2:7;
for x, y being set st x in [#] (product F1) & y in [#] (product F1) holds
f1 . (x,y) = f2 . (x,y)

proof

let x0, y0 be set ; :: thesis: ( x0 in [#] (product F1) & y0 in [#] (product F1) implies f1 . (x0,y0) = f2 . (x0,y0) )
assume A8: ( x0 in [#] (product F1) & y0 in [#] (product F1) ) ; :: thesis: f1 . (x0,y0) = f2 . (x0,y0)
then reconsider x1 = x0, y1 = y0 as Element of (product F1) ;
reconsider x2 = x0, y2 = y0 as Element of (product F2) by A2, A8;
A9: dom (x1 * y1) = I by GROUP_19:3;
A10: for i being object st i in dom (x1 * y1) holds
(x1 * y1) . i = (x2 * y2) . i

proof

let i be object ; :: thesis: ( i in dom (x1 * y1) implies (x1 * y1) . i = (x2 * y2) . i )
assume i in dom (x1 * y1) ; :: thesis: (x1 * y1) . i = (x2 * y2) . i
then reconsider i = i as Element of I by GROUP_19:3;
x1 in product F1 ;
then x1 . i in F1 . i by GROUP_19:5;
then reconsider x1i = x1 . i as Element of (F1 . i) ;
x2 in product F2 ;
then x2 . i in F2 . i by GROUP_19:5;
then reconsider x2i = x2 . i as Element of (F2 . i) ;
y1 in product F1 ;
then y1 . i in F1 . i by GROUP_19:5;
then reconsider y1i = y1 . i as Element of (F1 . i) ;
y2 in product F2 ;
then y2 . i in F2 . i by GROUP_19:5;
then reconsider y2i = y2 . i as Element of (F2 . i) ;
A11: F1 . i is Subgroup of F2 . i by A1;
(x1 * y1) . i = x1i * y1i by GROUP_7:1
.= x2i * y2i by A11, GROUP_2:43
.= (x2 * y2) . i by GROUP_7:1 ;
hence (x1 * y1) . i = (x2 * y2) . i ; :: thesis: verum

end;

A12: f2 . (x2,y2) = ( the multF of (product F2) | [:([#] (product F1)),([#] (product F1)):]) . [x2,y2] by BINOP_1:def 1
.= the multF of (product F2) . [x2,y2] by A8, FUNCT_1:49, ZFMISC_1:87
.= the multF of (product F2) . (x2,y2) by BINOP_1:def 1 ;
thus f1 . (x0,y0) = x1 * y1 by ALGSTR_0:def 18
.= x2 * y2 by A9, A10, GROUP_19:3
.= f2 . (x0,y0) by A12, ALGSTR_0:def 18 ; :: thesis: verum

end;

hence product F1 is Subgroup of product F2 by A7, BINOP_1:def 21, GROUP_2:def 5; :: thesis: verum