let I be non empty set ; :: thesis: for G being Group
for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a

let G be Group; :: thesis: for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a

let F be Subgroup-Family of I,G; :: thesis: for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a

let h be Homomorphism of (sum F),G; :: thesis: for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a

let a be finite-support Function of I,G; :: thesis: ( a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) implies h . a = Product a )

assume that
A1: a in sum F and
A2: for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ; :: thesis: h . a = Product a
A3: for i being object st i in I holds
F . i is Subgroup of G by Def1;
defpred S1[ Nat] means for b being finite-support Function of I,G st b in sum F & card () = \$1 holds
h . b = Product b;
A4: S1[ 0 ]
proof
let b be finite-support Function of I,G; :: thesis: ( b in sum F & card () = 0 implies h . b = Product b )
assume b in sum F ; :: thesis: ( not card () = 0 or h . b = Product b )
assume card () = 0 ; :: thesis: h . b = Product b
then A5: support b = {} ;
then b = 1_ () by
.= 1_ (sum F) by GROUP_2:44 ;
then h . b = 1_ G by GROUP_6:31;
hence h . b = Product b by ; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
let b be finite-support Function of I,G; :: thesis: ( b in sum F & card () = k + 1 implies h . b = Product b )
assume A8: b in sum F ; :: thesis: ( not card () = k + 1 or h . b = Product b )
assume A9: card () = k + 1 ; :: thesis: h . b = Product b
then not support b is empty ;
then consider i being object such that
A10: i in support b by XBOOLE_0:def 1;
A11: ( b . i <> 1_ G & i in I ) by ;
reconsider i = i as Element of I by A10;
set c = b +* (i,(1_ (F . i)));
b +* (i,(1_ (F . i))) in sum F by ;
then reconsider c = b +* (i,(1_ (F . i))) as Element of (sum F) ;
F . i is Subgroup of G by Def1;
then A12: 1_ (F . i) = 1_ G by GROUP_2:44;
then reconsider c0 = c as finite-support Function of I,G by GROUP_19:26;
A13: b in product F by ;
A14: b . i in F . i by ;
then (1ProdHom (F,i)) . (b . i) in ProjGroup (F,i) by FUNCT_2:5;
then (1ProdHom (F,i)) . (b . i) in sum F by GROUP_2:40;
then reconsider d = (1ProdHom (F,i)) . (b . i) as Element of (sum F) ;
A15: d = (1_ ()) +* (i,(b . i)) by ;
A16: d is Element of () by GROUP_2:42;
A17: support (d,F) = {i} by ;
A18: i in dom b by ;
A19: b = c * d
proof
reconsider c1 = c, d1 = d as Element of () by GROUP_2:42;
A20: support (c1,F) misses support (d1,F)
proof
c . i = 1_ (F . i) by ;
then for G being Group holds
( not G = F . i or not c . i <> 1_ G or not i in I ) ;
then not i in support (c,F) by GROUP_19:def 1;
hence support (c1,F) misses support (d1,F) by ; :: thesis: verum
end;
A21: dom (i .--> (b . i)) = {i} ;
A22: dom (1_ ()) = I by GROUP_19:3;
A23: d1 | (support (d1,F)) = ((1_ ()) +* (i,(b . i))) | {i} by
.= ((1_ ()) +* (i .--> (b . i))) | {i} by
.= i .--> (b . i) by ;
A24: i in dom c by ;
thus b = c1 +* (i,(b . i)) by Th7
.= c1 +* (d1 | (support (d1,F))) by
.= c1 * d1 by
.= c * d by GROUP_2:43 ; :: thesis: verum
end;
A25: h . c0 = Product c0
proof
A26: c0 in sum F ;
card (support c0) = (card ()) - 1 by
.= k by A9 ;
hence h . c0 = Product c0 by ; :: thesis: verum
end;
for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
proof
let i, j be Element of I; :: thesis: for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi

let gi, gj be Element of G; :: thesis: ( i <> j & gi in F . i & gj in F . j implies gi * gj = gj * gi )
assume that
A27: i <> j and
A28: gi in F . i and
A29: gj in F . j ; :: thesis: gi * gj = gj * gi
set ai = (1ProdHom (F,i)) . gi;
A30: (1ProdHom (F,i)) . gi in ProjGroup (F,i) by ;
then (1ProdHom (F,i)) . gi in sum F by GROUP_2:40;
then reconsider ai = (1ProdHom (F,i)) . gi as Element of (sum F) ;
reconsider bi = ai as Element of () by GROUP_2:42;
set aj = (1ProdHom (F,j)) . gj;
A31: (1ProdHom (F,j)) . gj in ProjGroup (F,j) by ;
then (1ProdHom (F,j)) . gj in sum F by GROUP_2:40;
then reconsider aj = (1ProdHom (F,j)) . gj as Element of (sum F) ;
reconsider bj = aj as Element of () by GROUP_2:42;
A32: gi = h . ai by ;
gi * gj = (h . ai) * (h . aj) by A2, A29, A32
.= h . (ai * aj) by GROUP_6:def 6
.= h . (bi * bj) by GROUP_2:43
.= h . (bj * bi) by
.= h . (aj * ai) by GROUP_2:43
.= (h . aj) * (h . ai) by GROUP_6:def 6
.= gj * gi by A2, A29, A32 ;
hence gi * gj = gj * gi ; :: thesis: verum
end;
then A33: F is component-commutative ;
A34: b in product F by ;
h . b = (h . c) * (h . d) by
.= (Product c0) * (b . i) by A2, A14, A25
.= Product b by ;
hence h . b = Product b ; :: thesis: verum
end;
A35: for k being Nat holds S1[k] from NAT_1:sch 2(A4, A6);
consider k being Nat such that
A36: card () = k ;
thus h . a = Product a by A1, A35, A36; :: thesis: verum