let I be non empty set ; :: thesis: for G being Group
for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) )
let G be Group; :: thesis: for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) )
let F be Group-Family of I; :: thesis: ( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) )
hereby :: thesis: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) implies F is internal DirectSumComponents of G,I )
assume A0: F is internal DirectSumComponents of G,I ; :: thesis: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) )
then A1: ( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st
( h is bijective & ( for a being finite-support Function of I,G st a in sum F holds
h . a = Product a ) ) ) by Def9;
A2: for i being object st i in I holds
F . i is Subgroup of G by A0, Def9;
consider h being Homomorphism of (sum F),G such that
A3: ( h is bijective & ( for a being finite-support Function of I,G st a in sum F holds
h . a = Product a ) ) by A0, Def9;
A4: for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x )
proof
let y be Element of G; :: thesis: ex x being finite-support Function of I,G st
( x in sum F & y = Product x )
rng h = the carrier of G by A3, FUNCT_2:def 3;
then consider x being Element of (sum F) such that
A5: y = h . x by FUNCT_2:113;
x in sum F ;
then reconsider x = x as finite-support Function of I,G by A2, Th10;
take x ; :: thesis: ( x in sum F & y = Product x )
thus x in sum F ; :: thesis: y = Product x
hence y = Product x by A3, A5; :: thesis: verum
end;
A6: for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2
proof
let x1, x2 be finite-support Function of I,G; :: thesis: ( x1 in sum F & x2 in sum F & Product x1 = Product x2 implies x1 = x2 )
assume A7: ( x1 in sum F & x2 in sum F & Product x1 = Product x2 ) ; :: thesis: x1 = x2
reconsider sx1 = x1, sx2 = x2 as Element of (sum F) by A7;
h . sx1 = Product x1 by A3, A7
.= h . sx2 by A3, A7 ;
hence x1 = x2 by A3, FUNCT_2:19; :: 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
A10: i <> j and
A11: gi in F . i and
A12: gj in F . j ; :: thesis: gi * gj = gj * gi
set xi = (1_ (product F)) +* (i,gi);
set xj = (1_ (product F)) +* (j,gj);
1_ (sum F) = 1_ (product F) by GROUP_2:44;
then A13: 1_ (product F) in sum F ;
then A14: (1_ (product F)) +* (i,gi) in sum F by A11, Th25;
A15: (1_ (product F)) +* (j,gj) in sum F by A12, A13, Th25;
reconsider xi = (1_ (product F)) +* (i,gi) as finite-support Function of I,G by A2, A11, A13, Th10, Th25;
reconsider xj = (1_ (product F)) +* (j,gj) as finite-support Function of I,G by A2, A12, A13, Th10, Th25;
reconsider sxi = xi as Element of (sum F) by A14;
reconsider sxj = xj as Element of (sum F) by A15;
reconsider pxi = sxi as Element of (product F) by GROUP_2:42;
reconsider pxj = sxj as Element of (product F) by GROUP_2:42;
xi = (I --> (1_ G)) +* (i,gi) by A1, Th13;
then A17: Product xi = gi by Th21;
xj = (I --> (1_ G)) +* (j,gj) by A1, Th13;
then A18: Product xj = gj by Th21;
A19: support (pxi,F) misses support (pxj,F)
proof
A20: support (pxi,F) c= {i} by A11, Th17;
support (pxj,F) c= {j} by A12, Th17;
hence support (pxi,F) misses support (pxj,F) by A10, A20, ZFMISC_1:11, XBOOLE_1:64; :: thesis: verum
end;
gi * gj = (h . sxi) * gj by A3, A11, A13, A17, Th25
.= (h . sxi) * (h . sxj) by A3, A12, A13, A18, Th25
.= h . (sxi * sxj) by GROUP_6:def 6
.= h . (pxi * pxj) by GROUP_2:43
.= h . (pxj * pxi) by A19, Th32
.= h . (sxj * sxi) by GROUP_2:43
.= (h . sxj) * (h . sxi) by GROUP_6:def 6
.= gj * (h . sxi) by A3, A12, A13, A18, Th25
.= gj * gi by A3, A11, A13, A17, Th25 ;
hence gi * gj = gj * gi ; :: thesis: verum
end;
hence ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) by A0, A4, A6, Def9; :: thesis: verum
end;
assume A32: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) ; :: thesis: F is internal DirectSumComponents of G,I
A33: for i being object st i in I holds
F . i is Subgroup of G by A32;
defpred S1[ object , object ] means ex x being finite-support Function of I,G st
( $1 = x & $2 = Product x );
A34: for x being Element of (sum F) ex y being Element of G st S1[x,y]
proof
let x be Element of (sum F); :: thesis: ex y being Element of G st S1[x,y]
x in sum F ;
then reconsider x = x as finite-support Function of I,G by A33, Th10;
Product x is Element of G ;
hence ex y being Element of G st S1[x,y] ; :: thesis: verum
end;
consider h being Function of (sum F),G such that
A35: for x being Element of (sum F) holds S1[x,h . x] from FUNCT_2:sch 3(A34);
 for y being object st y in [#] G holds
ex x being object st
( x in [#] (sum F) & y = h . x )
proof
let y be object ; :: thesis: ( y in [#] G implies ex x being object st
( x in [#] (sum F) & y = h . x ) )
assume y in [#] G ; :: thesis: ex x being object st
( x in [#] (sum F) & y = h . x )
then reconsider y = y as Element of G ;
consider x being finite-support Function of I,G such that
A36: ( x in sum F & y = Product x ) by A32;
ex x0 being finite-support Function of I,G st
( x = x0 & h . x = Product x0 ) by A35, A36;
hence ex x being object st
( x in [#] (sum F) & y = h . x ) by A36; :: thesis: verum
end;
then rng h = [#] G by FUNCT_2:10;
then A38: h is onto by FUNCT_2:def 3;
for x1, x2 being object st x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 implies x1 = x2 )
assume A39: ( x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 ) ; :: thesis: x1 = x2
then reconsider sx1 = x1, sx2 = x2 as Element of (sum F) ;
x1 in sum F by A39;
then reconsider x1 = x1 as finite-support Function of I,G by A33, Th10;
x2 in sum F by A39;
then reconsider x2 = x2 as finite-support Function of I,G by A33, Th10;
A40: ex x being finite-support Function of I,G st
( x1 = x & h . x1 = Product x ) by A35, A39;
A42: ex x being finite-support Function of I,G st
( x2 = x & h . x2 = Product x ) by A35, A39;
( x1 in sum F & x2 in sum F ) by A39;
hence x1 = x2 by A32, A39, A40, A42; :: thesis: verum
end;
then A43: h is one-to-one by FUNCT_2:19;
A44: for a being finite-support Function of I,G st a in sum F holds
h . a = Product a
proof
let a be finite-support Function of I,G; :: thesis: ( a in sum F implies h . a = Product a )
assume a in sum F ; :: thesis: h . a = Product a
then reconsider sa = a as Element of (sum F) ;
ex x being finite-support Function of I,G st
( sa = x & h . sa = Product x ) by A35;
hence h . a = Product a ; :: thesis: verum
end;
for x, y being Element of (sum F) holds h . (x * y) = (h . x) * (h . y)
proof
let x, y be Element of (sum F); :: thesis: h . (x * y) = (h . x) * (h . y)
consider x0 being finite-support Function of I,G such that
A45: ( x = x0 & h . x = Product x0 ) by A35;
consider y0 being finite-support Function of I,G such that
A46: ( y = y0 & h . y = Product y0 ) by A35;
consider xy0 being finite-support Function of I,G such that
A47: ( x * y = xy0 & h . (x * y) = Product xy0 ) by A35;
thus h . (x * y) = (h . x) * (h . y) by A32, A45, A46, A47, Th53; :: thesis: verum
end;
then reconsider h = h as Homomorphism of (sum F),G by GROUP_6:def 6;
h is bijective by A38, A43;
hence F is internal DirectSumComponents of G,I by A32, A44, Def8, Def9; :: thesis: verum