set GP = product F;
set CF = Carrier F;
A1: dom (Carrier F) = I by PARTFUN1:def 2;
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;
A2: dom g = dom (Carrier F) by CARD_3:9;
defpred S₁[ object ] means ex J being finite Subset of I ex f being ManySortedSet of J st
( $1 = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) );
consider A being set such that
A3: for x being object holds
( x in A iff ( x in product (Carrier F) & S₁[x] ) ) from XBOOLE_0:sch 1();
A4: A c= the carrier of (product F)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in the carrier of (product F) )
assume a in A ; :: thesis: a in the carrier of (product F)
then a in product (Carrier F) by A3;
hence a in the carrier of (product F) by Def2; :: thesis: verum

end;

A5: S₁[g]

proof

set J = {} I;
dom {} = {} I ;
then reconsider f = {} as ManySortedSet of {} I by PARTFUN1:def 2, RELAT_1:def 18;
take {} I ; :: thesis: ex f being ManySortedSet of {} I st
( g = g +* f & ( for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take f ; :: thesis: ( g = g +* f & ( for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
thus g = g +* {}
.= g +* f ; :: thesis: for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
thus for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; :: thesis: verum

end;

then reconsider A = A as non empty set by A3;
set b = the multF of (product F) || A;
A6: for p being Element of product (Carrier F) holds dom p = I by PARTFUN1:def 2;
( dom ( the multF of (product F) || A) = [:A,A:] & rng ( the multF of (product F) || A) c= A )

proof

dom the multF of (product F) = [: the carrier of (product F), the carrier of (product F):] by FUNCT_2:def 1;
hence A7: dom ( the multF of (product F) || A) = [:A,A:] by A4, RELAT_1:62, ZFMISC_1:96; :: thesis: rng ( the multF of (product F) || A) c= A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the multF of (product F) || A) or y in A )
assume y in rng ( the multF of (product F) || A) ; :: thesis: y in A
then consider x being object such that
A8: x in dom ( the multF of (product F) || A) and
A9: ( the multF of (product F) || A) . x = y by FUNCT_1:def 3;
consider x1, x2 being object such that
A10: x1 in A and
A11: x2 in A and
A12: x = [x1,x2] by A7, A8, ZFMISC_1:def 2;
consider J1 being finite Subset of I, f1 being ManySortedSet of J1 such that
A13: x1 = g +* f1 and
A14: for j being set st j in J1 holds
ex G being non empty Group-like multMagma st
( G = F . j & f1 . j in the carrier of G & f1 . j <> 1_ G ) by A3, A10;
consider J2 being finite Subset of I, f2 being ManySortedSet of J2 such that
A15: x2 = g +* f2 and
A16: for j being set st j in J2 holds
ex G being non empty Group-like multMagma st
( G = F . j & f2 . j in the carrier of G & f2 . j <> 1_ G ) by A3, A11;
reconsider x1 = x1, x2 = x2 as Function by A13, A15;
A17: dom f1 = J1 by PARTFUN1:def 2;

A18: now :: thesis: for i being object st i in I holds
x1 . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies x1 . b₁ in (Carrier F) . b₁ )
assume A19: i in I ; :: thesis: x1 . b₁ in (Carrier F) . b₁
then A20: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;

per cases ( i in J1 or not i in J1 ) ;

suppose A21: i in J1 ; :: thesis: x1 . b₁ in (Carrier F) . b₁

then ex G being non empty Group-like multMagma st
( G = F . i & f1 . i in the carrier of G & f1 . i <> 1_ G ) by A14;
hence x1 . i in (Carrier F) . i by A13, A17, A20, A21, FUNCT_4:13; :: thesis: verum

end;

suppose A22: not i in J1 ; :: thesis: x1 . b₁ in (Carrier F) . b₁

consider G being non empty Group-like multMagma such that
A23: G = F . i by A19, Def3;
x1 . i = g . i by A13, A17, A22, FUNCT_4:11
.= 1_ G by A19, A23, Th6 ;
hence x1 . i in (Carrier F) . i by A20, A23; :: thesis: verum

end;

end;

end;

A24: dom f2 = J2 by PARTFUN1:def 2;

A25: now :: thesis: for i being object st i in I holds
x2 . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies x2 . b₁ in (Carrier F) . b₁ )
assume A26: i in I ; :: thesis: x2 . b₁ in (Carrier F) . b₁
then A27: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;

per cases ( i in J2 or not i in J2 ) ;

suppose A28: i in J2 ; :: thesis: x2 . b₁ in (Carrier F) . b₁

then ex G being non empty Group-like multMagma st
( G = F . i & f2 . i in the carrier of G & f2 . i <> 1_ G ) by A16;
hence x2 . i in (Carrier F) . i by A15, A24, A27, A28, FUNCT_4:13; :: thesis: verum

end;

suppose A29: not i in J2 ; :: thesis: x2 . b₁ in (Carrier F) . b₁

consider G being non empty Group-like multMagma such that
A30: G = F . i by A26, Def3;
x2 . i = g . i by A15, A24, A29, FUNCT_4:11
.= 1_ G by A26, A30, Th6 ;
hence x2 . i in (Carrier F) . i by A27, A30; :: thesis: verum

end;

end;

end;

A31: dom x1 = (dom g) \/ (dom f1) by A13, FUNCT_4:def 1
.= I by A2, A1, A17, XBOOLE_1:12 ;
dom x2 = (dom g) \/ (dom f2) by A15, FUNCT_4:def 1
.= I by A2, A1, A24, XBOOLE_1:12 ;
then reconsider x2 = x2 as Element of product (Carrier F) by A1, A25, CARD_3:9;
reconsider x1 = x1 as Element of product (Carrier F) by A1, A31, A18, CARD_3:9;
reconsider X1 = x1, X2 = x2 as Element of (product F) by Def2;
A32: [x1,x2] in [:A,A:] by A10, A11, ZFMISC_1:87;
then A33: y = X1 * X2 by A9, A12, FUNCT_1:49;
then reconsider y1 = y as Element of product (Carrier F) by Def2;
defpred S₂[ object ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st
( G = F . $1 & k1 = x1 . $1 & k2 = x2 . $1 & k1 * k2 = 1_ G & f1 . $1 <> 1_ G & f2 . $1 <> 1_ G );
consider K being set such that
A34: for k being object holds
( k in K iff ( k in I & S₂[k] ) ) from XBOOLE_0:sch 1();
A35: S₁[y]

proof

defpred S₃[ object , object ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st
( G = F . $1 & k1 = x1 . $1 & k2 = x2 . $1 & $2 = k1 * k2 );
reconsider J = (J1 \/ J2) \ K as finite Subset of I ;
take J ; :: thesis: ex f being ManySortedSet of J st
( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
A36: dom y1 = I by A6;
A37: for j being object st j in J holds
ex t being object st S₃[j,t]

proof

let j be object ; :: thesis: ( j in J implies ex t being object st S₃[j,t] )
assume A38: j in J ; :: thesis: ex t being object st S₃[j,t]
then consider G being non empty Group-like multMagma such that
A39: G = F . j by Def3;
reconsider k1 = x1 . j, k2 = x2 . j as Element of G by A38, A39, Lm1;
take k1 * k2 ; :: thesis: S₃[j,k1 * k2]
thus S₃[j,k1 * k2] by A39; :: thesis: verum

end;

consider f being ManySortedSet of J such that
A40: for j being object st j in J holds
S₃[j,f . j] from PBOOLE:sch 3(A37);
take f ; :: thesis: ( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
set gf = g +* f;
A41: dom f = J by PARTFUN1:def 2;

A42: now :: thesis: for i being object st i in I holds
y1 . i = (g +* f) . i

let i be object ; :: thesis: ( i in I implies y1 . b₁ = (g +* f) . b₁ )
assume A43: i in I ; :: thesis: y1 . b₁ = (g +* f) . b₁
then consider Fi being non empty multMagma , h being Function such that
A44: Fi = F . i and
A45: h = the multF of (product F) . (x1,x2) and
A46: h . i = the multF of Fi . ((x1 . i),(x2 . i)) by Def2;
consider FF being non empty Group-like multMagma such that
A47: FF = F . i by A43, Def3;
reconsider Fi = Fi as non empty Group-like multMagma by A44, A47;
reconsider x1i = x1 . i, x2i = x2 . i as Element of Fi by A43, A44, Lm1;
A48: y1 . i = x1i * x2i by A9, A12, A32, A45, A46, FUNCT_1:49;

per cases ( i in J or not i in J ) ;

suppose A49: i in J ; :: thesis: y1 . b₁ = (g +* f) . b₁

then ex GG being non empty Group-like multMagma ex k1a, k2a being Element of GG st
( GG = F . i & k1a = x1 . i & k2a = x2 . i & f . i = k1a * k2a ) by A40;
hence y1 . i = (g +* f) . i by A33, A41, A44, A45, A46, A49, FUNCT_4:13; :: thesis: verum

end;

suppose A50: not i in J ; :: thesis: y1 . b₁ = (g +* f) . b₁

then A51: (g +* f) . i = g . i by A41, FUNCT_4:11
.= 1_ FF by A43, A47, Th6 ;

now :: thesis: ( ( not i in J1 \/ J2 & y1 . i = (g +* f) . i ) or ( i in K & y1 . i = (g +* f) . i ) )

per cases ( not i in J1 \/ J2 or i in K ) by A50, XBOOLE_0:def 5;

case A52: not i in J1 \/ J2 ; :: thesis: y1 . i = (g +* f) . i

then not i in J2 by XBOOLE_0:def 3;
then x2 . i = g . i by A15, A24, FUNCT_4:11;
then A53: x2 . i = 1_ FF by A43, A47, Th6;
not i in J1 by A52, XBOOLE_0:def 3;
then x1 . i = g . i by A13, A17, FUNCT_4:11;
then x1 . i = 1_ FF by A43, A47, Th6;
hence y1 . i = (g +* f) . i by A44, A47, A48, A51, A53, GROUP_1:def 4; :: thesis: verum

end;

case i in K ; :: thesis: y1 . i = (g +* f) . i

then ex GG being non empty Group-like multMagma ex k1, k2 being Element of GG st
( GG = F . i & k1 = x1 . i & k2 = x2 . i & k1 * k2 = 1_ GG & f1 . i <> 1_ GG & f2 . i <> 1_ GG ) by A34;
hence y1 . i = (g +* f) . i by A33, A43, A47, A51, Th1; :: thesis: verum

end;

end;

end;

hence y1 . i = (g +* f) . i ; :: thesis: verum

end;

end;

end;

dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1
.= I by A2, A1, A41, XBOOLE_1:12 ;
hence y = g +* f by A36, A42, FUNCT_1:2; :: thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
let j be set ; :: thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) )
assume A54: j in J ; :: thesis: ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
then consider G being non empty Group-like multMagma , k1, k2 being Element of G such that
A55: G = F . j and
A56: k1 = x1 . j and
A57: k2 = x2 . j and
A58: f . j = k1 * k2 by A40;
take G ; :: thesis: ( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
thus G = F . j by A55; :: thesis: ( f . j in the carrier of G & f . j <> 1_ G )
thus f . j in the carrier of G by A58; :: thesis: f . j <> 1_ G
A59: j in J1 \/ J2 by A54, XBOOLE_0:def 5;

per cases ( ( j in J1 & not j in J2 ) or ( not j in J1 & j in J2 ) or ( j in J1 & j in J2 ) ) by A59, XBOOLE_0:def 3;

suppose A60: ( j in J1 & not j in J2 ) ; :: thesis: f . j <> 1_ G

then A61: x1 . j = f1 . j by A13, A17, FUNCT_4:13;
consider G1 being non empty Group-like multMagma such that
A62: G1 = F . j and
f1 . j in the carrier of G1 and
A63: f1 . j <> 1_ G1 by A14, A60;
x2 . j = g . j by A15, A24, A60, FUNCT_4:11
.= 1_ G1 by A54, A62, Th6 ;
hence f . j <> 1_ G by A55, A56, A57, A58, A61, A62, A63, GROUP_1:def 4; :: thesis: verum

end;

suppose A64: ( not j in J1 & j in J2 ) ; :: thesis: f . j <> 1_ G

then A65: x2 . j = f2 . j by A15, A24, FUNCT_4:13;
consider G2 being non empty Group-like multMagma such that
A66: G2 = F . j and
f2 . j in the carrier of G2 and
A67: f2 . j <> 1_ G2 by A16, A64;
x1 . j = g . j by A13, A17, A64, FUNCT_4:11
.= 1_ G2 by A54, A66, Th6 ;
hence f . j <> 1_ G by A55, A56, A57, A58, A65, A66, A67, GROUP_1:def 4; :: thesis: verum

end;

suppose A68: ( j in J1 & j in J2 ) ; :: thesis: f . j <> 1_ G

then A69: ex G2 being non empty Group-like multMagma st
( G2 = F . j & f2 . j in the carrier of G2 & f2 . j <> 1_ G2 ) by A16;
A70: not j in K by A54, XBOOLE_0:def 5;
ex G1 being non empty Group-like multMagma st
( G1 = F . j & f1 . j in the carrier of G1 & f1 . j <> 1_ G1 ) by A14, A68;
hence f . j <> 1_ G by A34, A54, A55, A56, A57, A58, A69, A70; :: thesis: verum

end;

end;

end;

reconsider ff = X1 * X2 as Element of product (Carrier F) by Def2;

now :: thesis: ex J being finite Subset of I st
for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )

reconsider J = {} as finite Subset of I by XBOOLE_1:2;
take J = J; :: thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
thus for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ; :: thesis: verum

end;

hence y in A by A3, A33, A35; :: thesis: verum

end;

then reconsider b = the multF of (product F) || A as BinOp of A by FUNCT_2:def 1, RELSET_1:4;
set H = multMagma(# A,b #);
multMagma(# A,b #) is Group-like

proof

reconsider e = g as Element of multMagma(# A,b #) by A3, A5;
take e ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of multMagma(# A,b #) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# A,b #) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of multMagma(# A,b #); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of multMagma(# A,b #) st
( h * b₁ = e & b₁ * h = e ) )
reconsider h1 = h as Element of (product F) by A4;
[h,e] in [:A,A:] by ZFMISC_1:87;
hence h * e = h1 * (1_ (product F)) by FUNCT_1:49
.= h by GROUP_1:def 4 ;
:: thesis: ( e * h = h & ex b₁ being Element of the carrier of multMagma(# A,b #) st
( h * b₁ = e & b₁ * h = e ) )
[e,h] in [:A,A:] by ZFMISC_1:87;
hence e * h = (1_ (product F)) * h1 by FUNCT_1:49
.= h by GROUP_1:def 4 ;
:: thesis: ex b₁ being Element of the carrier of multMagma(# A,b #) st
( h * b₁ = e & b₁ * h = e )
reconsider h2 = h1, hh = h1 " as Element of product (Carrier F) by Def2;
A71: S₁[h1 " ]

proof

consider J being finite Subset of I, f being ManySortedSet of J such that
A72: h = g +* f and
A73: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) by A3;
defpred S₂[ object , object ] means ex G being Group ex m being Element of G st
( G = F . $1 & m = f . $1 & $2 = m " );
A74: for i being object st i in J holds
ex j being object st S₂[i,j]

proof

let i be object ; :: thesis: ( i in J implies ex j being object st S₂[i,j] )
assume A75: i in J ; :: thesis: ex j being object st S₂[i,j]
then consider Gg being non empty Group-like multMagma such that
A76: Gg = F . i by Def3;
ex Ga being non empty associative multMagma st Ga = F . i by A75, Def4;
then reconsider G = Gg as Group by A76;
ex GG being non empty Group-like multMagma st
( GG = F . i & f . i in the carrier of GG & f . i <> 1_ GG ) by A73, A75;
then reconsider m = f . i as Element of G by A76;
take m " ; :: thesis: S₂[i,m " ]
thus S₂[i,m " ] by A76; :: thesis: verum

end;

consider f9 being ManySortedSet of J such that
A77: for j being object st j in J holds
S₂[j,f9 . j] from PBOOLE:sch 3(A74);
set gf9 = g +* f9;
A78: dom f9 = J by PARTFUN1:def 2;
A79: dom f = J by PARTFUN1:def 2;

A80: now :: thesis: for i being object st i in I holds
hh . i = (g +* f9) . i

let i be object ; :: thesis: ( i in I implies hh . b₁ = (g +* f9) . b₁ )
assume A81: i in I ; :: thesis: hh . b₁ = (g +* f9) . b₁
then consider G3 being non empty Group-like multMagma such that
A82: G3 = F . i by Def3;
ex G4 being non empty associative multMagma st G4 = F . i by A81, Def4;
then consider G5 being Group such that
A83: G5 = F . i by A82;

per cases ( i in J or not i in J ) ;

suppose A84: i in J ; :: thesis: hh . b₁ = (g +* f9) . b₁

then A85: (g +* f9) . i = f9 . i by A78, FUNCT_4:13;
A86: ex G being Group ex m being Element of G st
( G = F . i & m = f . i & f9 . i = m " ) by A77, A84;
h2 . i = f . i by A72, A79, A84, FUNCT_4:13;
hence hh . i = (g +* f9) . i by A81, A86, A85, Th8; :: thesis: verum

end;

suppose A87: not i in J ; :: thesis: hh . b₁ = (g +* f9) . b₁

then A88: (g +* f9) . i = g . i by A78, FUNCT_4:11
.= 1_ G3 by A81, A82, Th6 ;
A89: 1_ G5 = (1_ G5) " by GROUP_1:8;
h2 . i = g . i by A72, A79, A87, FUNCT_4:11
.= 1_ G3 by A81, A82, Th6 ;
hence hh . i = (g +* f9) . i by A81, A82, A83, A88, A89, Th8; :: thesis: verum

end;

end;

end;

take J ; :: thesis: ex f being ManySortedSet of J st
( h1 " = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take f9 ; :: thesis: ( h1 " = g +* f9 & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) ) )
A90: dom hh = I by A6;
dom (g +* f9) = (dom g) \/ (dom f9) by FUNCT_4:def 1
.= I by A2, A1, A78, XBOOLE_1:12 ;
hence h1 " = g +* f9 by A90, A80; :: thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
let j be set ; :: thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) )
assume A91: j in J ; :: thesis: ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
then consider G being Group, m being Element of G such that
A92: G = F . j and
A93: m = f . j and
A94: f9 . j = m " by A77;
take G ; :: thesis: ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
thus ( G = F . j & f9 . j in the carrier of G ) by A92, A94; :: thesis: f9 . j <> 1_ G
ex G1 being non empty Group-like multMagma st
( G1 = F . j & f . j in the carrier of G1 & f . j <> 1_ G1 ) by A73, A91;
hence f9 . j <> 1_ G by A92, A93, A94, GROUP_1:10; :: thesis: verum

end;

product (Carrier F) = the carrier of (product F) by Def2;
then reconsider h9 = h1 " as Element of multMagma(# A,b #) by A3, A71;
take h9 ; :: thesis: ( h * h9 = e & h9 * h = e )
[h,h9] in [:A,A:] by ZFMISC_1:87;
hence h * h9 = h1 * (h1 ") by FUNCT_1:49
.= e by GROUP_1:def 5 ;
:: thesis: h9 * h = e
[h9,h] in [:A,A:] by ZFMISC_1:87;
hence h9 * h = (h1 ") * h1 by FUNCT_1:49
.= e by GROUP_1:def 5 ;
:: thesis: verum

end;

then reconsider H = multMagma(# A,b #) as non empty Group-like multMagma ;
reconsider H = H as strict Subgroup of product F by A4, GROUP_2:def 5;
take H ; :: thesis: for x being object holds
( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
let x be object ; :: thesis: ( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )

hereby :: thesis: ( ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) implies x in the carrier of H )

assume x in the carrier of H ; :: thesis: ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
then S₁[x] by A3;
hence ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ; :: thesis: verum

end;

given g being Element of product (Carrier F), J being finite Subset of I, f being ManySortedSet of J such that A95: g = 1_ (product F) and
A96: x = g +* f and
A97: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; :: thesis: x in the carrier of H
A98: dom g = I by A6;
set gf = g +* f;
A99: dom f = J by PARTFUN1:def 2;

A100: now :: thesis: for i being object st i in I holds
(g +* f) . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies (g +* f) . b₁ in (Carrier F) . b₁ )
assume A101: i in I ; :: thesis: (g +* f) . b₁ in (Carrier F) . b₁
then A102: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;

per cases ( i in J or not i in J ) ;

suppose A103: i in J ; :: thesis: (g +* f) . b₁ in (Carrier F) . b₁

then ex G being non empty Group-like multMagma st
( G = F . i & f . i in the carrier of G & f . i <> 1_ G ) by A97;
hence (g +* f) . i in (Carrier F) . i by A99, A102, A103, FUNCT_4:13; :: thesis: verum

end;

suppose A104: not i in J ; :: thesis: (g +* f) . b₁ in (Carrier F) . b₁

consider G being non empty Group-like multMagma such that
A105: G = F . i by A101, Def3;
(g +* f) . i = g . i by A99, A104, FUNCT_4:11
.= 1_ G by A95, A101, A105, Th6 ;
hence (g +* f) . i in (Carrier F) . i by A102, A105; :: thesis: verum

end;

end;

end;

dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1
.= I by A98, A99, XBOOLE_1:12 ;
then x in product (Carrier F) by A1, A96, A100, CARD_3:9;
hence x in the carrier of H by A3, A95, A96, A97; :: thesis: verum