let I be non empty set ; :: thesis:
let G be Group; :: thesis:
let F be Group-Family of I; :: thesis:

assume A0: F is internal DirectSumComponents of G,I ; :: thesis:
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 )

let y be Element of G; :: thesis:
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:
thus x in sum F ; :: thesis:
hence y = Product x by A3, A5; :: thesis:

end;

let x1, x2 be finite-support Function of I,G; :: thesis:
assume A7: ( x1 in sum F & x2 in sum F & Product x1 = Product x2 ) ; :: thesis:
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:

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

let i, j be Element of I; :: thesis:
let gi, gj be Element of G; :: thesis:
assume that
A10: i <> j and
A11: gi in F . i and
A12: gj in F . j ; :: thesis:
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)

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:

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:

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:
A33: for i being object st i in I holds
F . i is Subgroup of G by A32;
defpred S₁[ 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 S₁[x,y]

let x be Element of (sum F); :: thesis:
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 S₁[x,y] ; :: thesis:

end;

consider h being Function of (sum F),G such that
A35: for x being Element of (sum F) holds S₁[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 )

let y be object ; :: thesis:
assume y in [#] G ; :: thesis:
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:

end;

let x1, x2 be object ; :: thesis:
assume A39: ( x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 ) ; :: thesis:
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:

end;

let a be finite-support Function of I,G; :: thesis:
assume a in sum F ; :: thesis:
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:

end;

for x, y being Element of (sum F) holds h . (x * y) = (h . x) * (h . y)

let x, y be Element of (sum F); :: thesis:
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:

end;