let I be non empty set ; :: thesis:
let G be strict Group; :: thesis:
let F be Group-Family of I; :: thesis:
A1: dom F = I by PARTFUN1:def 2;
A2: dom (Carrier F) = I by PARTFUN1:def 2;

hereby :: thesis:

assume A3: F is internal DirectSumComponents of G,I ; :: thesis:
then A4: ( ( for i being object st i in 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 GROUP_19:54;
then A5: F is component-commutative Subgroup-Family of I,G by Def1, Def2;
for x being object st x in Union (Carrier F) holds
x in [#] G

proof

let x be object ; :: thesis:
assume x in Union (Carrier F) ; :: thesis:
then x in union (rng (Carrier F)) by CARD_3:def 4;
then consider Fi being set such that
A6: ( x in Fi & Fi in rng (Carrier F) ) by TARSKI:def 4;
consider i being object such that
A7: ( i in I & Fi = (Carrier F) . i ) by A2, A6, FUNCT_1:def 3;
reconsider i = i as Element of I by A7;
A8: (Carrier F) . i = [#] (F . i) by PENCIL_3:7;
F . i is Subgroup of G by A3, GROUP_19:54;
then [#] (F . i) c= [#] G by GROUP_2:def 5;
hence x in [#] G by A6, A7, A8; :: thesis:

end;

then Union (Carrier F) c= [#] G ;
then reconsider UF = Union (Carrier F) as Subset of G ;
A9: for g being Element of G holds g in gr UF

proof

let g be Element of G; :: thesis:
consider x being finite-support Function of I,G such that
A10: ( x in sum F & g = Product x ) by A3, GROUP_19:54;
x is Function of I,(Union (Carrier F)) by A10, GROUP_2:41, Th2;
then A11: rng x c= UF by RELAT_1:def 19;
UF c= [#] (gr UF) by GROUP_4:def 4;
then rng x c= [#] (gr UF) by A11;
then reconsider x0 = x as finite-support Function of I,(gr UF) by Th5;
reconsider fx = (x0 | (support x0)) * (canFS (support x0)) as FinSequence of (gr UF) by FINSEQ_2:32;
Product fx = Product x0 by GROUP_17:def 1
.= g by A10, Th6 ;
hence g in gr UF ; :: thesis:

end;

then A12: gr UF = G by GROUP_2:62;
thus for i being Element of I holds F . i is normal Subgroup of G by A5, A12, Th14; :: thesis:
thus ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) by A9, GROUP_2:62; :: thesis:
thus for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) :: thesis:

proof

let i be Element of I; :: thesis:
A13: for i being Element of I holds F . i is Subgroup of G by A3, GROUP_19:54;

per cases ;

suppose I \ {i} = {} ; :: thesis:

then A14: Union ((Carrier F) | (I \ {i})) = Union ((Carrier F) | {})
.= union (rng {}) by CARD_3:def 4
.= {} by ZFMISC_1:2 ;
reconsider UFi = {} the carrier of G as Subset of G ;
reconsider Fi = F . i as Subgroup of G by A3, GROUP_19:54;
gr UFi = (1). G by GROUP_4:30;
then A15: (gr UFi) /\ Fi = (1). G by GROUP_2:85;
([#] (gr UFi)) /\ ([#] Fi) = (carr (gr UFi)) /\ (carr Fi)
.= carr ((1). G) by A15, GROUP_2:81
.= {(1_ G)} by GROUP_2:def 7 ;
hence ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) by A14; :: thesis:

end;

suppose A16: I \ {i} <> {} ; :: thesis:

set CFi = (Carrier F) | (I \ {i});
set UFi = Union ((Carrier F) | (I \ {i}));
for x being object st x in Union ((Carrier F) | (I \ {i})) holds
x in [#] G

proof

let x be object ; :: thesis:
assume x in Union ((Carrier F) | (I \ {i})) ; :: thesis:
then x in union (rng ((Carrier F) | (I \ {i}))) by CARD_3:def 4;
then consider Fi being set such that
A17: ( x in Fi & Fi in rng ((Carrier F) | (I \ {i})) ) by TARSKI:def 4;
A18: dom ((Carrier F) | (I \ {i})) = I \ {i} by A2, RELAT_1:62;
consider j being object such that
A19: ( j in I \ {i} & Fi = ((Carrier F) | (I \ {i})) . j ) by A17, A18, FUNCT_1:def 3;
reconsider j = j as Element of I by A19;
A20: ((Carrier F) | (I \ {i})) . j = (Carrier F) . j by A19, FUNCT_1:49
.= [#] (F . j) by PENCIL_3:7 ;
F . j is Subgroup of G by A3, GROUP_19:54;
then [#] (F . j) c= [#] G by GROUP_2:def 5;
hence x in [#] G by A17, A19, A20; :: thesis:

end;

then reconsider UFi = Union ((Carrier F) | (I \ {i})) as Subset of G by TARSKI:def 3;
take UFi ; :: thesis:
thus UFi = Union ((Carrier F) | (I \ {i})) ; :: thesis:
A21: 1_ G in gr UFi by GROUP_2:46;
F . i is Subgroup of G by A3, GROUP_19:54;
then 1_ G in F . i by GROUP_2:46;
then 1_ G in ([#] (gr UFi)) /\ ([#] (F . i)) by A21, XBOOLE_0:def 4;
then A22: {(1_ G)} c= ([#] (gr UFi)) /\ ([#] (F . i)) by ZFMISC_1:31;
for x being object st x in ([#] (gr UFi)) /\ ([#] (F . i)) holds
x in {(1_ G)}

proof

let x be object ; :: thesis:
assume A23: x in ([#] (gr UFi)) /\ ([#] (F . i)) ; :: thesis:
then ( x in [#] (gr UFi) & x in [#] (F . i) ) by XBOOLE_0:def 4;
then reconsider g = x as Element of G by GROUP_2:def 5, TARSKI:def 3;
set I0 = I \ {i};
set F0 = F | (I \ {i});
A24: dom (F | (I \ {i})) = I \ {i} by A1, RELAT_1:62;
A25: for j being object st j in I \ {i} holds
(F | (I \ {i})) . j is Subgroup of G

proof

let j be object ; :: thesis:
assume A26: j in I \ {i} ; :: thesis:
then A27: F . j = (F | (I \ {i})) . j by FUNCT_1:49;
reconsider j = j as Element of I by A26;
(F | (I \ {i})) . j is Subgroup of G by A3, A27, GROUP_19:54;
hence (F | (I \ {i})) . j is Subgroup of G ; :: thesis:

end;

then for j being object st j in I \ {i} holds
(F | (I \ {i})) . j is Group ;
then reconsider F0 = F | (I \ {i}) as Group-Family of I \ {i} by A24, GROUP_19:2;
reconsider F0 = F0 as Subgroup-Family of I \ {i},G by A25, Def1;
A29: F0 is component-commutative

proof

let j, k be object ; :: according to GROUP_20:def 2 :: thesis:
let gj, gk be Element of G; :: thesis:
assume A28: ( j in I \ {i} & k in I \ {i} & j <> k ) ; :: thesis:
then reconsider Fj = F0 . j, Fk = F0 . k as Subgroup of G by Def1;
take Fj ; :: thesis:
take Fk ; :: thesis:
thus ( Fj = F0 . j & Fk = F0 . k ) ; :: thesis:
assume A29: ( gj in Fj & gk in Fk ) ; :: thesis:
reconsider j = j, k = k as Element of I by A28;
( F0 . j = F . j & F0 . k = F . k ) by A28, FUNCT_1:49;
hence gj * gk = gk * gj by A3, A28, A29, GROUP_19:54; :: thesis:

end;

A30: dom (Carrier F0) = I \ {i} by PARTFUN1:def 2;
for j being object st j in dom ((Carrier F) | (I \ {i})) holds
((Carrier F) | (I \ {i})) . j = (Carrier F0) . j

proof

let j be object ; :: thesis:
assume A31: j in dom ((Carrier F) | (I \ {i})) ; :: thesis:
then A32: j in I \ {i} ;
then reconsider I0 = I \ {i} as non empty set ;
reconsider F0 = F0 as Group-Family of I0 ;
reconsider j0 = j as Element of I0 by A31;
reconsider j = j as Element of I by A32;
((Carrier F) | (I \ {i})) . j = (Carrier F) . j by A31, FUNCT_1:49
.= [#] (F . j) by PENCIL_3:7
.= [#] (F0 . j0) by FUNCT_1:49
.= (Carrier F0) . j by PENCIL_3:7 ;
hence ((Carrier F) | (I \ {i})) . j = (Carrier F0) . j ; :: thesis:

end;

then A33: UFi = Union (Carrier F0) by A2, A30, FUNCT_1:2, RELAT_1:62;
g in gr UFi by A23, XBOOLE_0:def 4;
then consider hi being finite-support Function of (I \ {i}),(gr UFi) such that
A34: ( hi in sum F0 & g = Product hi ) by A16, A29, A33, Th13;
set h = hi +* ({i} --> (1_ G));
A35: rng (hi +* ({i} --> (1_ G))) c= (rng hi) \/ (rng ({i} --> (1_ G))) by FUNCT_4:17;
rng hi c= [#] G by GROUP_2:def 5, TARSKI:def 3;
then (rng hi) \/ (rng ({i} --> (1_ G))) c= [#] G by XBOOLE_1:8;
then A36: rng (hi +* ({i} --> (1_ G))) c= [#] G by A35;
A37: dom ({i} --> (1_ G)) = {i} ;
dom hi = I \ {i} by FUNCT_2:def 1;
then A38: dom (hi +* ({i} --> (1_ G))) = (I \ {i}) \/ {i} by A37, FUNCT_4:def 1
.= I by XBOOLE_1:45 ;
then reconsider h = hi +* ({i} --> (1_ G)) as Function of I,G by A36, FUNCT_2:2;
A39: for j being object holds
( j in support h iff j in support hi )

proof

let j be object ; :: thesis:

hereby :: thesis:

assume A40: j in support h ; :: thesis:
then A41: ( j in I & h . j <> 1_ G ) by GROUP_19:def 2;
A42: i <> j

proof

assume A43: j = i ; :: thesis:
then A44: j in {i} by TARSKI:def 1;
i in {i} by TARSKI:def 1;
then i in dom ({i} --> (1_ G)) ;
then h . j = ({i} --> (1_ G)) . j by A43, FUNCT_4:13
.= 1_ G by A44, FUNCOP_1:7 ;
hence contradiction by A40, GROUP_19:def 2; :: thesis:

end;

then not j in {i} by TARSKI:def 1;
then A45: j in I \ {i} by A40, XBOOLE_0:def 5;
not j in dom ({i} --> (1_ G)) by A42, TARSKI:def 1;
then hi . j <> 1_ G by A41, FUNCT_4:11;
then hi . j <> 1_ (gr UFi) by GROUP_2:44;
hence j in support hi by A45, GROUP_19:def 2; :: thesis:

end;

assume A46: j in support hi ; :: thesis:
then A47: ( j in I \ {i} & hi . j <> 1_ (gr UFi) ) by GROUP_19:def 2;
A48: ( j in I & not j in {i} ) by A46, XBOOLE_0:def 5;
not j in dom ({i} --> (1_ G)) by A46, XBOOLE_0:def 5;
then h . j = hi . j by FUNCT_4:11;
then h . j <> 1_ G by A47, GROUP_2:44;
hence j in support h by A48, GROUP_19:def 2; :: thesis:

end;

then A49: support h = support hi by TARSKI:2;
then reconsider h = h as finite-support Function of I,G by GROUP_19:def 3;
A50: support h = dom (h | (support h)) by PARTFUN1:def 2;
A51: support hi = dom (hi | (support hi)) by PARTFUN1:def 2;
for x being object st x in dom (h | (support h)) holds
(h | (support h)) . x = (hi | (support hi)) . x

proof

let x be object ; :: thesis:
assume A52: x in dom (h | (support h)) ; :: thesis:
x in dom (hi | (support hi)) by A39, A51, A52;
then A53: x in (dom hi) /\ (support hi) by RELAT_1:61;
A54: ( dom hi = I \ {i} & dom ({i} --> (1_ G)) = {i} ) by FUNCT_2:def 1;
thus (h | (support h)) . x = h . x by A52, FUNCT_1:47
.= hi . x by A53, A54, FUNCT_4:16, XBOOLE_1:79
.= (hi | (support hi)) . x by A39, A51, A52, FUNCT_1:47 ; :: thesis:

end;

then A55: h | (support h) = hi | (support hi) by A39, A50, A51, FUNCT_1:2, TARSKI:2;
reconsider fh = (h | (support h)) * (canFS (support h)) as FinSequence of G by FINSEQ_2:32;
reconsider fhi = (hi | (support hi)) * (canFS (support hi)) as FinSequence of (gr UFi) by FINSEQ_2:32;
A56: g = Product fhi by A34, GROUP_17:def 1
.= Product fh by A49, A55, GROUP_19:45
.= Product h by GROUP_17:def 1 ;
A57: i in {i} by TARSKI:def 1;
A58: dom ({i} --> (1_ G)) = {i} ;
A59: h in product F

proof

for j being object st j in I holds
h . j in (Carrier F) . j

proof

let j be object ; :: thesis:
assume j in I ; :: thesis:
then reconsider j = j as Element of I ;
h . j in [#] (F . j)

proof

per cases ;

suppose i = j ; :: thesis:

then A60: h . j = ({i} --> (1_ G)) . i by A57, A58, FUNCT_4:13
.= 1_ G by A57, FUNCOP_1:7 ;
F . j is Subgroup of G by A3, GROUP_19:54;
then 1_ G in F . j by GROUP_2:46;
hence h . j in [#] (F . j) by A60; :: thesis:

end;

suppose A61: i <> j ; :: thesis:

then not j in {i} by TARSKI:def 1;
then A62: j in I \ {i} by XBOOLE_0:def 5;
A63: not j in dom ({i} --> (1_ G)) by A61, TARSKI:def 1;
A64: h . j = hi . j by A63, FUNCT_4:11;
reconsider I0 = I \ {i} as non empty set by A62;
reconsider F0 = F0 as Group-Family of I0 ;
reconsider j0 = j as Element of I0 by A62;
hi . j0 in F0 . j0 by A34, GROUP_19:5, GROUP_2:40;
hence h . j in [#] (F . j) by A64, FUNCT_1:49; :: thesis:

end;

hence h . j in (Carrier F) . j by PENCIL_3:7; :: thesis:

end;

then h in product (Carrier F) by A2, A38, CARD_3:def 5;
hence h in product F by GROUP_7:def 2; :: thesis:

end;

A65: h in sum F

proof

reconsider h0 = h as Element of (product F) by A59;
support h = support (h0,F) by A4, GROUP_19:9;
hence h in sum F by GROUP_19:8; :: thesis:

end;

reconsider id1g = I --> (1_ G) as Function of I,G ;
support id1g is empty by GROUP_19:12;
then reconsider id1g = id1g as finite-support Function of I,G by GROUP_19:def 3;
A66: 1_ (product F) = id1g by A13, GROUP_19:13;
then reconsider k = (1_ (product F)) +* (i,g) as finite-support Function of I,G by GROUP_19:26;
A67: Product k = g by A66, GROUP_19:21;
k in ProjSet (F,i) by A23, GROUP_12:def 1;
then k in ProjGroup (F,i) by GROUP_12:def 2;
then A68: k in sum F by GROUP_2:40;
dom (1_ (product F)) = I by GROUP_19:3;
then g = k . i by FUNCT_7:31
.= h . i by A3, A56, A65, A67, A68, GROUP_19:54
.= ({i} --> (1_ G)) . i by A57, A58, FUNCT_4:13
.= 1_ G by A57, FUNCOP_1:7 ;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis:

end;

then ([#] (gr UFi)) /\ ([#] (F . i)) c= {(1_ G)} ;
hence ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A22, XBOOLE_0:def 10; :: thesis:

end;

assume that
A69: for i being Element of I holds F . i is normal Subgroup of G and
A70: ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) and
A71: for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ; :: thesis:
consider UF being Subset of G such that
A72: ( UF = Union (Carrier F) & gr UF = G ) by A70;
A73: for i being Element of I holds F . i is Subgroup of G by A69;
A74: for i being object st i in I holds
F . i is Subgroup of G by A69;
A75: for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

proof

let i, j be Element of I; :: thesis:
assume A76: i <> j ; :: thesis:
F . i is Subgroup of G by A69;
then 1_ G in F . i by GROUP_2:46;
then A77: {(1_ G)} c= [#] (F . i) by ZFMISC_1:31;
F . j is Subgroup of G by A69;
then 1_ G in F . j by GROUP_2:46;
then {(1_ G)} c= [#] (F . j) by ZFMISC_1:31;
then A78: {(1_ G)} c= ([#] (F . i)) /\ ([#] (F . j)) by A77, XBOOLE_1:19;
for x being object st x in ([#] (F . i)) /\ ([#] (F . j)) holds
x in {(1_ G)}

proof

let x be object ; :: thesis:
assume A79: x in ([#] (F . i)) /\ ([#] (F . j)) ; :: thesis:
then A80: ( x in [#] (F . i) & x in [#] (F . j) ) by XBOOLE_0:def 4;
consider UFj being Subset of G such that
A81: ( UFj = Union ((Carrier F) | (I \ {j})) & ([#] (gr UFj)) /\ ([#] (F . j)) = {(1_ G)} ) by A71;
( i in I & not i in {j} ) by A76, TARSKI:def 1;
then A82: i in I \ {j} by XBOOLE_0:def 5;
A83: i in dom ((Carrier F) | (I \ {j})) by A2, A82, RELAT_1:62;
((Carrier F) | (I \ {j})) . i = (Carrier F) . i by A82, FUNCT_1:49
.= [#] (F . i) by PENCIL_3:7 ;
then [#] (F . i) c= union (rng ((Carrier F) | (I \ {j}))) by A83, FUNCT_1:3, ZFMISC_1:74;
then A84: [#] (F . i) c= UFj by A81, CARD_3:def 4;
UFj c= [#] (gr UFj) by GROUP_4:def 4;
then x in [#] (gr UFj) by A80, A84;
hence x in {(1_ G)} by A79, A81, XBOOLE_0:def 4; :: thesis:

end;

then ([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)} ;
hence ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by A78, XBOOLE_0:def 10; :: thesis:

end;

A85: 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:
let gi, gj be Element of G; :: thesis:
assume A86: ( i <> j & gi in F . i & gj in F . j ) ; :: thesis:
A87: F . i is normal Subgroup of G by A69;
A88: F . j is normal Subgroup of G by A69;
A89: ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by A75, A86;
set x = (gi * gj) * ((gj * gi) ");
A90: gi " in F . i by A86, A87, GROUP_2:51;
A91: gj " in F . j by A86, A88, GROUP_2:51;
A92: (gi * gj) * (gi ") in F . j by A86, A88, Th1;
A93: gj * ((gi ") * (gj ")) in F . i by A87, A90, Th1;
(gi * gj) * ((gj * gi) ") = (gi * gj) * ((gi ") * (gj ")) by GROUP_1:17
.= ((gi * gj) * (gi ")) * (gj ") by GROUP_1:def 3 ;
then A94: (gi * gj) * ((gj * gi) ") in F . j by A88, A91, A92, GROUP_2:50;
(gi * gj) * ((gj * gi) ") = (gi * gj) * ((gi ") * (gj ")) by GROUP_1:17
.= gi * (gj * ((gi ") * (gj "))) by GROUP_1:def 3 ;
then (gi * gj) * ((gj * gi) ") in F . i by A86, A87, A93, GROUP_2:50;
then (gi * gj) * ((gj * gi) ") in ([#] (F . i)) /\ ([#] (F . j)) by A94, XBOOLE_0:def 4;
then (gi * gj) * ((gj * gi) ") = 1_ G by A89, TARSKI:def 1;
then (gi * gj) " = (gj * gi) " by GROUP_1:12;
hence gi * gj = gj * gi by GROUP_1:9; :: thesis:

end;

A95: F is component-commutative Subgroup-Family of I,G by A74, A85, Def1, Def2;
A96: 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:
y in gr UF by A72;
then consider x being finite-support Function of I,(gr UF) such that
A97: ( x in sum F & y = Product x ) by A72, A95, Th13;
reconsider x = x as finite-support Function of I,G by A72;
take x ; :: thesis:
thus ( x in sum F & y = Product x ) by A72, A97; :: thesis:

end;

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 A71, A95, Th15;
hence F is internal DirectSumComponents of G,I by A73, A85, A96, GROUP_19:54; :: thesis: