let I be non empty set ; :: thesis:
let G be Group; :: thesis:
let i be object ; :: thesis:
assume A1: i in I ; :: thesis:
set v = I --> ((1). G);
set w = {i} --> G;
set F = (I --> ((1). G)) +* ({i} --> G);
A4: dom ((I --> ((1). G)) +* ({i} --> G)) = (dom (I --> ((1). G))) \/ (dom ({i} --> G)) by FUNCT_4:def 1
.= (dom (I --> ((1). G))) \/ {i} by FUNCOP_1:13
.= I \/ {i} by FUNCOP_1:13
.= I by A1, XBOOLE_1:12, ZFMISC_1:31 ;
A5: i in {i} by TARSKI:def 1;
then i in dom ({i} --> G) by FUNCOP_1:13;
then A7: ((I --> ((1). G)) +* ({i} --> G)) . i = ({i} --> G) . i by FUNCT_4:13;
then A8: ((I --> ((1). G)) +* ({i} --> G)) . i = G by A5, FUNCOP_1:7;
A9: for j being object st j in I \ {i} holds
((I --> ((1). G)) +* ({i} --> G)) . j = (1). G

let j be object ; :: thesis:
assume A10: j in I \ {i} ; :: thesis:
then j in dom ((I --> ((1). G)) +* ({i} --> G)) by A4;
then A11: j in (dom (I --> ((1). G))) \/ (dom ({i} --> G)) by FUNCT_4:def 1;
not j in dom ({i} --> G) by A10, XBOOLE_0:def 5;
hence ((I --> ((1). G)) +* ({i} --> G)) . j = (I --> ((1). G)) . j by A11, FUNCT_4:def 1
.= (1). G by A10, FUNCOP_1:7 ;
:: thesis:

end;

for j being object st j in I holds
((I --> ((1). G)) +* ({i} --> G)) . j is Group

proof

let j be object ; :: thesis:
assume A12: j in I ; :: thesis:

per cases ;

suppose j in {i} ; :: thesis:

hence ((I --> ((1). G)) +* ({i} --> G)) . j is Group by A8, TARSKI:def 1; :: thesis:

end;

suppose not j in {i} ; :: thesis:

then j in I \ {i} by A12, XBOOLE_0:def 5;
hence ((I --> ((1). G)) +* ({i} --> G)) . j is Group by A9; :: thesis:

end;

then reconsider F = (I --> ((1). G)) +* ({i} --> G) as Group-Family of I by A4, Th2;
A17: for j being Element of I holds 1_ (F . j) = 1_ G

proof

let j be Element of I; :: thesis:

per cases ;

suppose j in {i} ; :: thesis:

hence 1_ (F . j) = 1_ G by A8, TARSKI:def 1; :: thesis:

end;

suppose not j in {i} ; :: thesis:

then j in I \ {i} by XBOOLE_0:def 5;
then F . j = (1). G by A9;
hence 1_ (F . j) = 1_ G by GROUP_2:44; :: thesis:

end;

defpred S₁[ Element of (sum F), Element of G] means $2 = $1 . i;
A24: for x being Element of (sum F) ex y being Element of G st S₁[x,y]

proof

let x be Element of (sum F); :: thesis:
B01: x in sum F ;
reconsider i = i as Element of I by A1;
A25: x . i in F . i by GROUP_2:40, Th5, B01;
A26: i in {i} by TARSKI:def 1;
then A27: i in dom ({i} --> G) by FUNCOP_1:13;
then i in (dom (I --> ((1). G))) \/ (dom ({i} --> G)) by XBOOLE_0:def 3;
then F . i = ({i} --> G) . i by A27, FUNCT_4:def 1;
then reconsider y = x . i as Element of G by A25, A26, FUNCOP_1:7;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

consider h being Function of (sum F),G such that
A29: for x being Element of (sum F) holds S₁[x,h . x] from FUNCT_2:sch 3(A24);
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:
assume A30: y in [#] G ; :: thesis:
reconsider i = i as Element of I by A1;
set x = (1_ (product F)) +* (i,y);
A32: 1_ (product F) in product F ;
A33: y in F . i by A5, A7, A30, FUNCOP_1:7;
then (1_ (product F)) +* (i,y) in product F by A32, Th24;
then reconsider x = (1_ (product F)) +* (i,y) as Element of (product F) ;
support (x,F) c= {i} by A33, Th17;
then A35: x in sum F by Th8;
take x ; :: thesis:
thus x in [#] (sum F) by A35; :: thesis:
A36: dom (1_ (product F)) = I by Th3;
reconsider x = x as Element of (sum F) by A35;
reconsider y = y as Element of G by A30;
S₁[x,y] by A36, FUNCT_7:31;
hence y = h . x by A29; :: thesis:

end;

then rng h = [#] G by FUNCT_2:10;
then A42: h is onto by FUNCT_2:def 3;
A43: for x being Element of (sum F) holds support (x,F) c= {i}

proof

let x be Element of (sum F); :: thesis:

now :: thesis:

let j be object ; :: thesis:
assume A44: j in support (x,F) ; :: thesis:
then consider Z being Group such that
A45: ( Z = F . j & x . j <> 1_ Z & j in I ) by Def1;
assume not j in {i} ; :: thesis:
then j in I \ {i} by A44, XBOOLE_0:def 5;
then A46: F . j = (1). G by A9;
x in sum F ;
then x . j in Z by A45, GROUP_2:40, Th5;
then x . j in {(1_ G)} by A45, A46, GROUP_2:def 7;
then x . j = 1_ G by TARSKI:def 1;
hence contradiction by A45, A46, GROUP_2:44; :: thesis:

end;

hence support (x,F) c= {i} ; :: thesis:

end;

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:
assume A48: ( x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 ) ; :: thesis:
then reconsider x1 = x1, x2 = x2 as Element of (sum F) ;
( x1 in sum F & x2 in sum F ) ;
then A49: ( x1 in product F & x2 in product F ) by GROUP_2:40;
then A50: ( dom x1 = I & dom x2 = I ) by Th3;
consider J1 being finite Subset of I, a1 being ManySortedSet of J1 such that
A51: ( J1 = support (x1,F) & x1 = (1_ (product F)) +* a1 & ( for j being object
for G being Group st j in I \ J1 & G = F . j holds
x1 . j = 1_ G ) & ( for j being object st j in J1 holds
x1 . j = a1 . j ) ) by Th7;
consider J2 being finite Subset of I, a2 being ManySortedSet of J2 such that
A52: ( J2 = support (x2,F) & x2 = (1_ (product F)) +* a2 & ( for j being object
for G being Group st j in I \ J2 & G = F . j holds
x2 . j = 1_ G ) & ( for j being object st j in J2 holds
x2 . j = a2 . j ) ) by Th7;
A53: support (x1,F) c= {i} by A43;
A54: support (x2,F) c= {i} by A43;
for j being object st j in dom x1 holds
x1 . j = x2 . j

proof

let j be object ; :: thesis:
assume j in dom x1 ; :: thesis:
then A56: j in I by A49, Th3;
then reconsider Z = F . j as Group by Th1;

per cases ;

suppose not j in {i} ; :: thesis:

then ( not j in J1 & not j in J2 ) by A51, A52, A53, A54;
then A59: ( j in I \ J1 & j in I \ J2 ) by A56, XBOOLE_0:def 5;
hence x1 . j = 1_ Z by A51
.= x2 . j by A52, A59 ;
:: thesis:

end;

suppose j in {i} ; :: thesis:

then A61: j = i by TARSKI:def 1;
hence x1 . j = h . x2 by A29, A48
.= x2 . j by A29, A61 ;
:: thesis:

end;

hence x1 = x2 by A50, FUNCT_1:2; :: thesis:

end;

then A62: h is one-to-one by FUNCT_2:19;
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:
A68: for j being set st j in I holds
ex Fi being non empty multMagma ex xi, yi being Element of Fi st
( xi = x . j & yi = y . j & Fi = F . j & (x * y) . j = xi * yi )

proof

let j be set ; :: thesis:
assume j in I ; :: thesis:
then reconsider j = j as Element of I ;
x in sum F ;
then x in product F by GROUP_2:40;
then reconsider x0 = x as Element of (product F) ;
x0 in product F ;
then x0 . j in F . j by Th5;
then reconsider xi = x0 . j as Element of (F . j) ;
y in sum F ;
then y in product F by GROUP_2:40;
then reconsider y0 = y as Element of (product F) ;
y0 in product F ;
then y0 . j in F . j by Th5;
then reconsider yi = y0 . j as Element of (F . j) ;
(x * y) . j = (x0 * y0) . j by GROUP_2:43
.= xi * yi by GROUP_7:1 ;
hence ex Fi being non empty multMagma ex xi, yi being Element of Fi st
( xi = x . j & yi = y . j & Fi = F . j & (x * y) . j = xi * yi ) ; :: thesis:

end;

h . (x * y) = (h . x) * (h . y)

proof

consider Fa being non empty multMagma , xa, ya being Element of Fa such that
A72: ( xa = x . i & ya = y . i & Fa = F . i & (x * y) . i = xa * ya ) by A1, A68;
A74: xa = h . x by A29, A72;
thus h . (x * y) = xa * ya by A29, A72
.= (h . x) * (h . y) by A8, A29, A72, A74 ; :: thesis:

end;

hence h . (x * y) = (h . x) * (h . y) ; :: thesis:

end;

then reconsider h = h as Homomorphism of (sum F),G by GROUP_6:def 6;
take F ; :: thesis:
take h ; :: thesis:
thus h is bijective by A42, A62; :: thesis:
thus F = (I --> ((1). G)) +* ({i} --> G) ; :: thesis:
thus for j being Element of I holds 1_ (F . j) = 1_ G by A17; :: thesis:
thus for x being Element of (sum F) holds h . x = x . i by A29; :: thesis:
let x be Element of (sum F); :: thesis:
A78: support (x,F) c= {i} by A43;
A79: ( support (x,F) = {} or support (x,F) = {i} )

proof

per cases ;

suppose support (x,F) = {} ; :: thesis:

hence ( support (x,F) = {} or support (x,F) = {i} ) ; :: thesis:

end;

suppose support (x,F) <> {} ; :: thesis:

then consider j being object such that
A82: j in support (x,F) by XBOOLE_0:def 1;
A83: {j} c= support (x,F) by A82, ZFMISC_1:31;
j = i by A78, A82, TARSKI:def 1;
hence ( support (x,F) = {} or support (x,F) = {i} ) by A78, A83, XBOOLE_0:def 10; :: thesis:

end;

consider J being finite Subset of I, a being ManySortedSet of J such that
A85: ( J = support (x,F) & x = (1_ (product F)) +* a & ( for j being object
for G being Group st j in I \ J & G = F . j holds
x . j = 1_ G ) & ( for j being object st j in J holds
x . j = a . j ) ) by Th7;
take J ; :: thesis:
take a ; :: thesis:
thus ( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) by A79, A85; :: thesis: