let G be Group; :: thesis:
let I1, I2 be non empty set ; :: thesis:
let F1 be DirectSumComponents of G,I1; :: thesis:
let F2 be Group-Family of I2; :: thesis:
assume that
A1: I1 misses I2 and
A2: for i being Element of I2 holds card (F2 . i) = 1 ; :: thesis:
reconsider I = {1,2} as non empty set ;
set J = {[1,I1],[2,I2]};
for x, y1, y2 being object st [x,y1] in {[1,I1],[2,I2]} & [x,y2] in {[1,I1],[2,I2]} holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis:
assume ( [x,y1] in {[1,I1],[2,I2]} & [x,y2] in {[1,I1],[2,I2]} ) ; :: thesis:
then A3: ( ( [x,y1] = [1,I1] or [x,y1] = [2,I2] ) & ( [x,y2] = [1,I1] or [x,y2] = [2,I2] ) ) by TARSKI:def 2;

per cases by XTUPLE_0:1;

suppose ( x = 1 & y1 = I1 ) ; :: thesis:

hence y1 = y2 by A3, XTUPLE_0:1; :: thesis:

end;

suppose ( x = 2 & y1 = I2 ) ; :: thesis:

hence y1 = y2 by A3, XTUPLE_0:1; :: thesis:

end;

then reconsider J = {[1,I1],[2,I2]} as Function by FUNCT_1:def 1;
dom J = I by RELAT_1:10;
then reconsider J = J as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A4: rng J = {I1,I2} by RELAT_1:10;
[1,I1] in J by TARSKI:def 2;
then A5: ( 1 in dom J & J . 1 = I1 ) by FUNCT_1:1;
[2,I2] in J by TARSKI:def 2;
then A6: ( 2 in dom J & J . 2 = I2 ) by FUNCT_1:1;
not {} in rng J

proof

assume {} in rng J ; :: thesis:
then consider x being object such that
A7: ( x in dom J & {} = J . x ) by FUNCT_1:def 3;
thus contradiction by A5, A6, A7, TARSKI:def 2; :: thesis:

end;

then J is non-empty ;
then reconsider J = J as non-empty ManySortedSet of I ;
for i, j being object st i <> j holds
J . i misses J . j

proof

let i, j be object ; :: thesis:
assume A8: i <> j ; :: thesis:

per cases ;

suppose ( not i in dom J or not j in dom J ) ; :: thesis:

then ( J . i = {} or J . j = {} ) by FUNCT_1:def 2;
then (J . i) /\ (J . j) = {} ;
hence J . i misses J . j by XBOOLE_0:def 7; :: thesis:

end;

suppose ( i in dom J & j in dom J ) ; :: thesis:

then ( ( i = 1 or i = 2 ) & ( j = 1 or j = 2 ) ) by TARSKI:def 2;
hence J . i misses J . j by A1, A5, A6, A8; :: thesis:

end;

then J is disjoint_valued ;
then reconsider J = J as non-empty disjoint_valued ManySortedSet of I ;
reconsider M = <*(sum F1),(sum F2)*> as Group-Family of I ;
set w0 = the object ;
card ([#] (sum F2)) = 1 by A2, Th43;
then card ([#] (sum F2)) = card { the object } by CARD_1:30;
then consider w being object such that
A9: {w} = [#] (sum F2) by CARD_1:29;
A10: for x, y being Function st x in [#] (product M) & y in [#] (product M) & x . 1 = y . 1 holds
x = y

proof

let x, y be Function; :: thesis:
assume that
A11: x in [#] (product M) and
A12: y in [#] (product M) and
A13: x . 1 = y . 1 ; :: thesis:
A14: ( dom x = I & dom y = I ) by A11, A12, GROUP_19:3;
for i being object st i in dom x holds
x . i = y . i

proof

let i be object ; :: thesis:
assume i in dom x ; :: thesis:
then A15: ( i = 1 or i = 2 ) by A14, TARSKI:def 2;
A16: ( x in product M & y in product M ) by A11, A12;
reconsider p = x, q = y as Function ;
B1: 2 is Element of I by TARSKI:def 2;
reconsider M2 = M . 2 as Group ;
( p . 2 in M2 & q . 2 in M2 ) by A16, B1, GROUP_19:5;
then ( p . 2 in sum F2 & q . 2 in sum F2 ) ;
then ( p . 2 = w & q . 2 = w ) by A9, TARSKI:def 1;
hence x . i = y . i by A13, A15; :: thesis:

end;

hence x = y by A14; :: thesis:

end;

consider h1 being Homomorphism of (sum F1),G such that
A17: h1 is bijective by GROUP_19:def 8;
set CS1 = the carrier of (product M);
set CS2 = the carrier of G;
defpred S₁[ Element of the carrier of (product M), Element of the carrier of G] means $2 = h1 . ($1 . 1);
A18: for x being Element of the carrier of (product M) ex y being Element of the carrier of G st S₁[x,y]

proof

let x be Element of the carrier of (product M); :: thesis:
A19: x in product M ;
reconsider x = x as Function ;
B1: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M . 1 as Group ;
x . 1 in M1 by B1, A19, GROUP_19:5;
then x . 1 in sum F1 ;
then h1 . (x . 1) in the carrier of G by FUNCT_2:5;
hence ex y being Element of the carrier of G st S₁[x,y] ; :: thesis:

end;

consider h being Function of the carrier of (product M), the carrier of G such that
A20: for x being Element of the carrier of (product M) holds S₁[x,h . x] from FUNCT_2:sch 3(A18);
reconsider h = h as Function of the carrier of (product M), the carrier of G ;
for x1, x2 being object st x1 in the carrier of (product M) & x2 in the carrier of (product M) & h . x1 = h . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume A21: ( x1 in the carrier of (product M) & x2 in the carrier of (product M) & h . x1 = h . x2 ) ; :: thesis:
then reconsider x10 = x1, x20 = x2 as Element of the carrier of (product M) ;
A22: h . x10 = h1 . (x10 . 1) by A20;
A23: h . x20 = h1 . (x20 . 1) by A20;
A24: ( x1 in product M & x2 in product M ) by A21;
reconsider z1 = x1 as Function by A21;
reconsider z2 = x2 as Function by A21;
B2: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M . 1 as Group ;
( z1 . 1 in M1 & z2 . 1 in M1 ) by A24, B2, GROUP_19:5;
then A25: ( x10 . 1 in the carrier of (sum F1) & x20 . 1 in the carrier of (sum F1) ) ;
x10 . 1 = x20 . 1 by A17, A21, A22, A23, A25, FUNCT_2:19;
hence x1 = x2 by A10; :: thesis:

end;

then A26: h is one-to-one by FUNCT_2:19;
for y being object st y in the carrier of G holds
ex x being object st
( x in the carrier of (product M) & y = h . x )

proof

let y be object ; :: thesis:
assume y in the carrier of G ; :: thesis:
then y in rng h1 by A17, FUNCT_2:def 3;
then consider x1 being object such that
A27: ( x1 in [#] (sum F1) & y = h1 . x1 ) by FUNCT_2:11;
reconsider x1 = x1 as Element of [#] (sum F1) by A27;
set z1 = the Element of [#] (sum F2);
reconsider x = <*x1, the Element of [#] (sum F2)*> as Element of the carrier of (product M) ;
take x ; :: thesis:
h . x = h1 . (x . 1) by A20
.= y by A27 ;
hence ( x in the carrier of (product M) & y = h . x ) ; :: thesis:

end;

then rng h = the carrier of G by FUNCT_2:10;
then A28: h is onto by FUNCT_2:def 3;
for a, b being Element of the carrier of (product M) holds h . (a * b) = (h . a) * (h . b)

proof

let a, b be Element of the carrier of (product M); :: thesis:
A29: 1 in I by TARSKI:def 2;
A30: M . 1 = sum F1 ;
A31: ( a in product M & b in product M ) ;
reconsider a1 = a, b1 = b as Function ;
B3: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M . 1 as Group ;
( a1 . 1 in M1 & b1 . 1 in M1 ) by B3, A31, GROUP_19:5;
then reconsider a1 = a . 1, b1 = b . 1 as Element of (sum F1) ;
thus h . (a * b) = h1 . ((a * b) . 1) by A20
.= h1 . (a1 * b1) by A29, A30, GROUP_7:1
.= (h1 . a1) * (h1 . b1) by GROUP_6:def 6
.= (h1 . a1) * (h . b) by A20
.= (h . a) * (h . b) by A20 ; :: thesis:

end;

then A32: h is Homomorphism of (product M),G by GROUP_6:def 6;
product M = sum M by GROUP_7:9;
then reconsider M = <*(sum F1),(sum F2)*> as DirectSumComponents of G,I by A26, A28, A32, GROUP_19:def 8;
set N = <*F1,F2*>;
len <*F1,F2*> = 2 by FINSEQ_1:44;
then dom <*F1,F2*> = I by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider N = <*F1,F2*> as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A33: for i being Element of I holds N . i is Group-Family of J . i

proof

let i be Element of I; :: thesis:

per cases by TARSKI:def 2;

suppose i = 1 ; :: thesis:

hence N . i is Group-Family of J . i by A5; :: thesis:

end;

suppose i = 2 ; :: thesis:

hence N . i is Group-Family of J . i by A6; :: thesis:

end;

then for i being Element of I holds N . i is multMagma-Family of J . i ;
then reconsider N = N as multMagma-Family of I,J by Def4;
reconsider N = N as Group-Family of I,J by A33, Def5;
A34: for i being Element of I holds N . i is DirectSumComponents of M . i,J . i

proof

let i be Element of I; :: thesis:

per cases by TARSKI:def 2;

suppose A35: i = 1 ; :: thesis:

set h = id the carrier of (sum F1);
for a, b being Element of (sum F1) holds (id the carrier of (sum F1)) . (a * b) = ((id the carrier of (sum F1)) . a) * ((id the carrier of (sum F1)) . b) ;
then A36: ( id the carrier of (sum F1) is Homomorphism of (sum F1),(sum F1) & id the carrier of (sum F1) is bijective ) by GROUP_6:def 6;
thus N . i is DirectSumComponents of M . i,J . i by A5, A35, A36, GROUP_19:def 8; :: thesis:

end;

suppose A38: i = 2 ; :: thesis:

set h = id the carrier of (sum F2);
for a, b being Element of (sum F2) holds (id the carrier of (sum F2)) . (a * b) = ((id the carrier of (sum F2)) . a) * ((id the carrier of (sum F2)) . b) ;
then A39: ( id the carrier of (sum F2) is Homomorphism of (sum F2),(sum F2) & id the carrier of (sum F2) is bijective ) by GROUP_6:def 6;
thus N . i is DirectSumComponents of M . i,J . i by A6, A38, A39, GROUP_19:def 8; :: thesis:

end;

A41: I1 \/ I2 = Union J by A4, ZFMISC_1:75;
A42: dom (Union N) = Union J by PARTFUN1:def 2
.= (dom F1) \/ I2 by A41, PARTFUN1:def 2
.= (dom F1) \/ (dom F2) by PARTFUN1:def 2 ;
for x being object st x in (dom F1) \/ (dom F2) holds
( ( x in dom F2 implies (Union N) . x = F2 . x ) & ( not x in dom F2 implies (Union N) . x = F1 . x ) )

proof

let x be object ; :: thesis:
assume x in (dom F1) \/ (dom F2) ; :: thesis:
then A43: x in I1 \/ (dom F2) by PARTFUN1:def 2;
then A44: x in I1 \/ I2 by PARTFUN1:def 2;
thus ( x in dom F2 implies (Union N) . x = F2 . x ) :: thesis:

proof

assume A45: x in dom F2 ; :: thesis:
then reconsider i = x as Element of Union J by A41, XBOOLE_0:def 3;
reconsider j = 2 as Element of I by TARSKI:def 2;
(Union N) . i = (N . j) . i by A6, A45, Th19
.= F2 . i ;
hence (Union N) . x = F2 . x ; :: thesis:

end;

thus ( not x in dom F2 implies (Union N) . x = F1 . x ) :: thesis:

proof

assume A46: not x in dom F2 ; :: thesis:
reconsider i = x as Element of Union J by A41, A43, PARTFUN1:def 2;
reconsider j = 1 as Element of I by TARSKI:def 2;
not x in I2 by A46, PARTFUN1:def 2;
then i in J . j by A5, A44, XBOOLE_0:def 3;
then (Union N) . i = (N . j) . i by Th19
.= F1 . i ;
hence (Union N) . x = F1 . x ; :: thesis:

end;

then F1 +* F2 = Union N by A42, FUNCT_4:def 1;
hence F1 +* F2 is DirectSumComponents of G,I1 \/ I2 by A34, A41, Th39; :: thesis: