let I be non empty set ; 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; ( ( 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
; product F1 is Subgroup of product F2
A2:
for x being object st x in [#] (product F1) holds
x in [#] (product F2)
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 ;
( 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) )
;
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
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
;
verum
end;
hence
product F1 is Subgroup of product F2
by A7, BINOP_1:def 21, GROUP_2:def 5; verum