let I be non empty set ; :: thesis: for G being strict 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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

let G be strict 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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

A1: dom F = I by PARTFUN1:def 2;

A2: dom (Carrier F) = I by PARTFUN1:def 2;

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: F is internal DirectSumComponents of G,I

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)}

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

gi * gj = gj * gi

A96: for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x )

x1 = x2 by A71, A95, Th15;

hence F is internal DirectSumComponents of G,I by A73, A85, A96, GROUP_19:54; :: thesis: verum

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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

let G be strict 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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) ) )

A1: dom F = I by PARTFUN1:def 2;

A2: dom (Carrier F) = I by PARTFUN1:def 2;

hereby :: thesis: ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) implies F is internal DirectSumComponents of G,I )

assume that ( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) implies F is internal DirectSumComponents of G,I )

assume A3:
F is internal DirectSumComponents of G,I
; :: thesis: ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) )

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

then reconsider UF = Union (Carrier F) as Subset of G ;

A9: for g being Element of G holds g in gr UF

thus for i being Element of I holds F . i is normal Subgroup of G by A5, A12, Th14; :: thesis: ( ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) )

thus ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) by A9, GROUP_2:62; :: thesis: 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)} )

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: verum

end;( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) )

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

then
Union (Carrier F) c= [#] G
;
let x be object ; :: thesis: ( x in Union (Carrier F) implies x in [#] G )

assume x in Union (Carrier F) ; :: thesis: x in [#] G

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: verum

end;assume x in Union (Carrier F) ; :: thesis: x in [#] G

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: verum

then reconsider UF = Union (Carrier F) as Subset of G ;

A9: for g being Element of G holds g in gr UF

proof

then A12:
gr UF = G
by GROUP_2:62;
let g be Element of G; :: thesis: g in gr UF

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: verum

end;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: verum

thus for i being Element of I holds F . i is normal Subgroup of G by A5, A12, Th14; :: thesis: ( ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( 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)} ) ) )

thus ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) by A9, GROUP_2:62; :: thesis: 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)} )

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: verum

proof

let i be Element of I; :: thesis: ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

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

end;( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

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

per cases
( I \ {i} = {} or I \ {i} <> {} )
;

end;

suppose
I \ {i} = {}
; :: thesis: ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

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: verum

end;.= 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: verum

suppose A16:
I \ {i} <> {}
; :: thesis: ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

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

take UFi ; :: thesis: ( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

thus UFi = Union ((Carrier F) | (I \ {i})) ; :: thesis: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)}

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)}

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

end;set UFi = Union ((Carrier F) | (I \ {i}));

for x being object st x in Union ((Carrier F) | (I \ {i})) holds

x in [#] G

proof

then reconsider UFi = Union ((Carrier F) | (I \ {i})) as Subset of G by TARSKI:def 3;
let x be object ; :: thesis: ( x in Union ((Carrier F) | (I \ {i})) implies x in [#] G )

assume x in Union ((Carrier F) | (I \ {i})) ; :: thesis: x in [#] G

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: verum

end;assume x in Union ((Carrier F) | (I \ {i})) ; :: thesis: x in [#] G

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: verum

take UFi ; :: thesis: ( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

thus UFi = Union ((Carrier F) | (I \ {i})) ; :: thesis: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)}

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

then
([#] (gr UFi)) /\ ([#] (F . i)) c= {(1_ G)}
;
let x be object ; :: thesis: ( x in ([#] (gr UFi)) /\ ([#] (F . i)) implies x in {(1_ G)} )

assume A23: x in ([#] (gr UFi)) /\ ([#] (F . i)) ; :: thesis: x in {(1_ G)}

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

(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

for j being object st j in dom ((Carrier F) | (I \ {i})) holds

((Carrier F) | (I \ {i})) . j = (Carrier F0) . j

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 )

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

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

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: verum

end;assume A23: x in ([#] (gr UFi)) /\ ([#] (F . i)) ; :: thesis: x in {(1_ G)}

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

then
for j being object st j in I \ {i} holds
let j be object ; :: thesis: ( j in I \ {i} implies (F | (I \ {i})) . j is Subgroup of G )

assume A26: j in I \ {i} ; :: thesis: (F | (I \ {i})) . j is Subgroup of G

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: verum

end;assume A26: j in I \ {i} ; :: thesis: (F | (I \ {i})) . j is Subgroup of G

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: verum

(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

A30:
dom (Carrier F0) = I \ {i}
by PARTFUN1:def 2;
let j, k be object ; :: according to GROUP_20:def 2 :: thesis: for gi, gj being Element of G st j in I \ {i} & k in I \ {i} & j <> k holds

ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )

let gj, gk be Element of G; :: thesis: ( j in I \ {i} & k in I \ {i} & j <> k implies ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) ) )

assume A28: ( j in I \ {i} & k in I \ {i} & j <> k ) ; :: thesis: ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) )

then reconsider Fj = F0 . j, Fk = F0 . k as Subgroup of G by Def1;

take Fj ; :: thesis: ex Fj being Subgroup of G st

( Fj = F0 . j & Fj = F0 . k & ( gj in Fj & gk in Fj implies gj * gk = gk * gj ) )

take Fk ; :: thesis: ( Fj = F0 . j & Fk = F0 . k & ( gj in Fj & gk in Fk implies gj * gk = gk * gj ) )

thus ( Fj = F0 . j & Fk = F0 . k ) ; :: thesis: ( gj in Fj & gk in Fk implies gj * gk = gk * gj )

assume A29: ( gj in Fj & gk in Fk ) ; :: thesis: gj * gk = gk * gj

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: verum

end;ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )

let gj, gk be Element of G; :: thesis: ( j in I \ {i} & k in I \ {i} & j <> k implies ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) ) )

assume A28: ( j in I \ {i} & k in I \ {i} & j <> k ) ; :: thesis: ex Fi, Fj being Subgroup of G st

( Fi = F0 . j & Fj = F0 . k & ( gj in Fi & gk in Fj implies gj * gk = gk * gj ) )

then reconsider Fj = F0 . j, Fk = F0 . k as Subgroup of G by Def1;

take Fj ; :: thesis: ex Fj being Subgroup of G st

( Fj = F0 . j & Fj = F0 . k & ( gj in Fj & gk in Fj implies gj * gk = gk * gj ) )

take Fk ; :: thesis: ( Fj = F0 . j & Fk = F0 . k & ( gj in Fj & gk in Fk implies gj * gk = gk * gj ) )

thus ( Fj = F0 . j & Fk = F0 . k ) ; :: thesis: ( gj in Fj & gk in Fk implies gj * gk = gk * gj )

assume A29: ( gj in Fj & gk in Fk ) ; :: thesis: gj * gk = gk * gj

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: verum

for j being object st j in dom ((Carrier F) | (I \ {i})) holds

((Carrier F) | (I \ {i})) . j = (Carrier F0) . j

proof

then A33:
UFi = Union (Carrier F0)
by A2, A30, FUNCT_1:2, RELAT_1:62;
let j be object ; :: thesis: ( j in dom ((Carrier F) | (I \ {i})) implies ((Carrier F) | (I \ {i})) . j = (Carrier F0) . j )

assume A31: j in dom ((Carrier F) | (I \ {i})) ; :: thesis: ((Carrier F) | (I \ {i})) . j = (Carrier F0) . j

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: verum

end;assume A31: j in dom ((Carrier F) | (I \ {i})) ; :: thesis: ((Carrier F) | (I \ {i})) . j = (Carrier F0) . j

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: verum

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

then A49:
support h = support hi
by TARSKI:2;
let j be object ; :: thesis: ( j in support h iff j in support hi )

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: verum

end;hereby :: thesis: ( j in support hi implies j in support h )

assume A46:
j in support hi
; :: thesis: j in support hassume A40:
j in support h
; :: thesis: j in support hi

then A41: ( j in I & h . j <> 1_ G ) by GROUP_19:def 2;

A42: i <> j

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: verum

end;then A41: ( j in I & h . j <> 1_ G ) by GROUP_19:def 2;

A42: i <> j

proof

then
not j in {i}
by TARSKI:def 1;
assume A43:
j = i
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

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: verum

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

then A55:
h | (support h) = hi | (support hi)
by A39, A50, A51, FUNCT_1:2, TARSKI:2;
let x be object ; :: thesis: ( x in dom (h | (support h)) implies (h | (support h)) . x = (hi | (support hi)) . x )

assume A52: x in dom (h | (support h)) ; :: thesis: (h | (support h)) . x = (hi | (support hi)) . x

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: verum

end;assume A52: x in dom (h | (support h)) ; :: thesis: (h | (support h)) . x = (hi | (support hi)) . x

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: verum

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

A65:
h in sum F
for j being object st j in I holds

h . j in (Carrier F) . j

hence h in product F by GROUP_7:def 2; :: thesis: verum

end;h . j in (Carrier F) . j

proof

then
h in product (Carrier F)
by A2, A38, CARD_3:def 5;
let j be object ; :: thesis: ( j in I implies h . j in (Carrier F) . j )

assume j in I ; :: thesis: h . j in (Carrier F) . j

then reconsider j = j as Element of I ;

h . j in [#] (F . j)

end;assume j in I ; :: thesis: h . j in (Carrier F) . j

then reconsider j = j as Element of I ;

h . j in [#] (F . j)

proof
end;

hence
h . j in (Carrier F) . j
by PENCIL_3:7; :: thesis: verumper cases
( i = j or i <> j )
;

end;

suppose
i = j
; :: thesis: h . j in [#] (F . j)

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: verum

end;.= 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: verum

suppose A61:
i <> j
; :: thesis: h . j in [#] (F . j)

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: verum

end;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: verum

hence h in product F by GROUP_7:def 2; :: thesis: verum

proof

reconsider id1g = I --> (1_ G) as Function of I,G ;
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: verum

end;support h = support (h0,F) by A4, GROUP_19:9;

hence h in sum F by GROUP_19:8; :: thesis: verum

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: verum

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

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: F is internal DirectSumComponents of G,I

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

A85:
for i, j being Element of I
let i, j be Element of I; :: thesis: ( i <> j implies ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} )

assume A76: i <> j ; :: thesis: ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

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)}

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

end;assume A76: i <> j ; :: thesis: ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

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

then
([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)}
;
let x be object ; :: thesis: ( x in ([#] (F . i)) /\ ([#] (F . j)) implies x in {(1_ G)} )

assume A79: x in ([#] (F . i)) /\ ([#] (F . j)) ; :: thesis: x in {(1_ G)}

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: verum

end;assume A79: x in ([#] (F . i)) /\ ([#] (F . j)) ; :: thesis: x in {(1_ G)}

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: verum

hence ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by A78, XBOOLE_0:def 10; :: 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

A95:
F is component-commutative Subgroup-Family of I,G
by A74, A85, Def1, Def2;
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 A86: ( i <> j & gi in F . i & gj in F . j ) ; :: thesis: gi * gj = gj * gi

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: 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 A86: ( i <> j & gi in F . i & gj in F . j ) ; :: thesis: gi * gj = gj * gi

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: verum

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

for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
let y be Element of G; :: thesis: ex x being finite-support Function of I,G st

( x in sum F & y = Product x )

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: ( x in sum F & y = Product x )

thus ( x in sum F & y = Product x ) by A72, A97; :: thesis: verum

end;( x in sum F & y = Product x )

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: ( x in sum F & y = Product x )

thus ( x in sum F & y = Product x ) by A72, A97; :: thesis: verum

x1 = x2 by A71, A95, Th15;

hence F is internal DirectSumComponents of G,I by A73, A85, A96, GROUP_19:54; :: thesis: verum