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 S_{1}[ Nat] means for b being finite-support Function of I,G st b in sum F & card (support b) = $1 holds

h . b = Product b;

A4: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A4, A6);

consider k being Nat such that

A36: card (support a) = k ;

thus h . a = Product a by A1, A35, A36; :: thesis: verum

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 S

h . b = Product b;

A4: S

proof

A6:
for k being Nat st S
let b be finite-support Function of I,G; :: thesis: ( b in sum F & card (support b) = 0 implies h . b = Product b )

assume b in sum F ; :: thesis: ( not card (support b) = 0 or h . b = Product b )

assume card (support b) = 0 ; :: thesis: h . b = Product b

then A5: support b = {} ;

then b = 1_ (product F) by A3, GROUP_19:14

.= 1_ (sum F) by GROUP_2:44 ;

then h . b = 1_ G by GROUP_6:31;

hence h . b = Product b by A5, GROUP_19:15; :: thesis: verum

end;assume b in sum F ; :: thesis: ( not card (support b) = 0 or h . b = Product b )

assume card (support b) = 0 ; :: thesis: h . b = Product b

then A5: support b = {} ;

then b = 1_ (product F) by A3, GROUP_19:14

.= 1_ (sum F) by GROUP_2:44 ;

then h . b = 1_ G by GROUP_6:31;

hence h . b = Product b by A5, GROUP_19:15; :: thesis: verum

S

proof

A35:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let b be finite-support Function of I,G; :: thesis: ( b in sum F & card (support b) = k + 1 implies h . b = Product b )

assume A8: b in sum F ; :: thesis: ( not card (support b) = k + 1 or h . b = Product b )

assume A9: card (support b) = 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 A10, GROUP_19:def 2;

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 A8, GROUP_19:25;

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 A8, GROUP_2:40;

A14: b . i in F . i by A8, GROUP_19:5, GROUP_2:40;

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_ (product F)) +* (i,(b . i)) by A14, GROUP_12:def 3;

A16: d is Element of (product F) by GROUP_2:42;

A17: support (d,F) = {i} by A11, A12, A14, A15, A16, GROUP_19:18;

A18: i in dom b by A11, A13, GROUP_19:3;

A19: b = c * d

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi

A34: b in product F by A8, GROUP_2:40;

h . b = (h . c) * (h . d) by A19, GROUP_6:def 6

.= (Product c0) * (b . i) by A2, A14, A25

.= Product b by A33, A34, Th8 ;

hence h . b = Product b ; :: thesis: verum

end;assume A7: S

let b be finite-support Function of I,G; :: thesis: ( b in sum F & card (support b) = k + 1 implies h . b = Product b )

assume A8: b in sum F ; :: thesis: ( not card (support b) = k + 1 or h . b = Product b )

assume A9: card (support b) = 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 A10, GROUP_19:def 2;

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 A8, GROUP_19:25;

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 A8, GROUP_2:40;

A14: b . i in F . i by A8, GROUP_19:5, GROUP_2:40;

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_ (product F)) +* (i,(b . i)) by A14, GROUP_12:def 3;

A16: d is Element of (product F) by GROUP_2:42;

A17: support (d,F) = {i} by A11, A12, A14, A15, A16, GROUP_19:18;

A18: i in dom b by A11, A13, GROUP_19:3;

A19: b = c * d

proof

A25:
h . c0 = Product c0
reconsider c1 = c, d1 = d as Element of (product F) by GROUP_2:42;

A20: support (c1,F) misses support (d1,F)

A22: dom (1_ (product F)) = I by GROUP_19:3;

A23: d1 | (support (d1,F)) = ((1_ (product F)) +* (i,(b . i))) | {i} by A11, A12, A14, A15, GROUP_19:18

.= ((1_ (product F)) +* (i .--> (b . i))) | {i} by A22, FUNCT_7:def 3

.= i .--> (b . i) by A21, FUNCT_4:23 ;

A24: i in dom c by A18, FUNCT_7:30;

thus b = c1 +* (i,(b . i)) by Th7

.= c1 +* (d1 | (support (d1,F))) by A23, A24, FUNCT_7:def 3

.= c1 * d1 by A20, GROUP_19:31

.= c * d by GROUP_2:43 ; :: thesis: verum

end;A20: support (c1,F) misses support (d1,F)

proof

A21:
dom (i .--> (b . i)) = {i}
;
c . i = 1_ (F . i)
by A18, FUNCT_7:31;

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 A17, ZFMISC_1:50; :: thesis: verum

end;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 A17, ZFMISC_1:50; :: thesis: verum

A22: dom (1_ (product F)) = I by GROUP_19:3;

A23: d1 | (support (d1,F)) = ((1_ (product F)) +* (i,(b . i))) | {i} by A11, A12, A14, A15, GROUP_19:18

.= ((1_ (product F)) +* (i .--> (b . i))) | {i} by A22, FUNCT_7:def 3

.= i .--> (b . i) by A21, FUNCT_4:23 ;

A24: i in dom c by A18, FUNCT_7:30;

thus b = c1 +* (i,(b . i)) by Th7

.= c1 +* (d1 | (support (d1,F))) by A23, A24, FUNCT_7:def 3

.= c1 * d1 by A20, GROUP_19:31

.= c * d by GROUP_2:43 ; :: thesis: verum

proof

for i, j being Element of I
A26:
c0 in sum F
;

card (support c0) = (card (support b)) - 1 by A10, A12, GROUP_19:30

.= k by A9 ;

hence h . c0 = Product c0 by A7, A26; :: thesis: verum

end;card (support c0) = (card (support b)) - 1 by A10, A12, GROUP_19:30

.= k by A9 ;

hence h . c0 = Product c0 by A7, A26; :: thesis: verum

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi

proof

then A33:
F is component-commutative
;
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 A28, FUNCT_2:5;

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 (product F) by GROUP_2:42;

set aj = (1ProdHom (F,j)) . gj;

A31: (1ProdHom (F,j)) . gj in ProjGroup (F,j) by A29, FUNCT_2:5;

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 (product F) by GROUP_2:42;

A32: gi = h . ai by A2, A28;

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 A27, A30, A31, GROUP_12:7

.= 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;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 A28, FUNCT_2:5;

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 (product F) by GROUP_2:42;

set aj = (1ProdHom (F,j)) . gj;

A31: (1ProdHom (F,j)) . gj in ProjGroup (F,j) by A29, FUNCT_2:5;

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 (product F) by GROUP_2:42;

A32: gi = h . ai by A2, A28;

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 A27, A30, A31, GROUP_12:7

.= 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

A34: b in product F by A8, GROUP_2:40;

h . b = (h . c) * (h . d) by A19, GROUP_6:def 6

.= (Product c0) * (b . i) by A2, A14, A25

.= Product b by A33, A34, Th8 ;

hence h . b = Product b ; :: thesis: verum

consider k being Nat such that

A36: card (support a) = k ;

thus h . a = Product a by A1, A35, A36; :: thesis: verum