set GP = product F;
set CF = Carrier F;
A1: dom () = I by PARTFUN1:def 2;
reconsider g = 1_ () as Element of product () by Def2;
A2: dom g = dom () by CARD_3:9;
defpred S1[ 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 () & S1[x] ) ) from A4: A c= the carrier of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in the carrier of () )
assume a in A ; :: thesis: a in the carrier of ()
then a in product () by A3;
hence a in the carrier of () by Def2; :: thesis: verum
end;
A5: S1[g]
proof
set J = {} I;
dom {} = {} I ;
then reconsider f = {} as ManySortedSet of {} I by ;
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 () || A;
A6: for p being Element of product () holds dom p = I by PARTFUN1:def 2;
( dom ( the multF of () || A) = [:A,A:] & rng ( the multF of () || A) c= A )
proof
dom the multF of () = [: the carrier of (), the carrier of ():] by FUNCT_2:def 1;
hence A7: dom ( the multF of () || A) = [:A,A:] by ; :: thesis: rng ( the multF of () || A) c= A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the multF of () || A) or y in A )
assume y in rng ( the multF of () || A) ; :: thesis: y in A
then consider x being object such that
A8: x in dom ( the multF of () || A) and
A9: ( the multF of () || 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 ;
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 ;
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 ;
reconsider x1 = x1, x2 = x2 as Function by ;
A17: dom f1 = J1 by PARTFUN1:def 2;
A18: now :: thesis: for i being object st i in I holds
x1 . i in () . i
let i be object ; :: thesis: ( i in I implies x1 . b1 in () . b1 )
assume A19: i in I ; :: thesis: x1 . b1 in () . b1
then A20: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by PRALG_1:def 13;
per cases ( i in J1 or not i in J1 ) ;
suppose A21: i in J1 ; :: thesis: x1 . b1 in () . b1
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 () . i by ; :: thesis: verum
end;
suppose A22: not i in J1 ; :: thesis: x1 . b1 in () . b1
consider G being non empty Group-like multMagma such that
A23: G = F . i by ;
x1 . i = g . i by
.= 1_ G by ;
hence x1 . i in () . i by ; :: 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 () . i
let i be object ; :: thesis: ( i in I implies x2 . b1 in () . b1 )
assume A26: i in I ; :: thesis: x2 . b1 in () . b1
then A27: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by PRALG_1:def 13;
per cases ( i in J2 or not i in J2 ) ;
suppose A28: i in J2 ; :: thesis: x2 . b1 in () . b1
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 () . i by ; :: thesis: verum
end;
suppose A29: not i in J2 ; :: thesis: x2 . b1 in () . b1
consider G being non empty Group-like multMagma such that
A30: G = F . i by ;
x2 . i = g . i by
.= 1_ G by ;
hence x2 . i in () . i by ; :: thesis: verum
end;
end;
end;
A31: dom x1 = (dom g) \/ (dom f1) by
.= I by ;
dom x2 = (dom g) \/ (dom f2) by
.= I by ;
then reconsider x2 = x2 as Element of product () by ;
reconsider x1 = x1 as Element of product () by ;
reconsider X1 = x1, X2 = x2 as Element of () by Def2;
A32: [x1,x2] in [:A,A:] by ;
then A33: y = X1 * X2 by ;
then reconsider y1 = y as Element of product () by Def2;
defpred S2[ 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 & S2[k] ) ) from A35: S1[y]
proof
defpred S3[ 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 S3[j,t]
proof
let j be object ; :: thesis: ( j in J implies ex t being object st S3[j,t] )
assume A38: j in J ; :: thesis: ex t being object st S3[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 ;
take k1 * k2 ; :: thesis: S3[j,k1 * k2]
thus S3[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
S3[j,f . j] from 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 . b1 = (g +* f) . b1 )
assume A43: i in I ; :: thesis: y1 . b1 = (g +* f) . b1
then consider Fi being non empty multMagma , h being Function such that
A44: Fi = F . i and
A45: h = the multF of () . (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 ;
reconsider Fi = Fi as non empty Group-like multMagma by ;
reconsider x1i = x1 . i, x2i = x2 . i as Element of Fi by ;
A48: y1 . i = x1i * x2i by ;
per cases ( i in J or not i in J ) ;
suppose A49: i in J ; :: thesis: y1 . b1 = (g +* f) . b1
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 ; :: thesis: verum
end;
suppose A50: not i in J ; :: thesis: y1 . b1 = (g +* f) . b1
then A51: (g +* f) . i = g . i by
.= 1_ FF by ;
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 ;
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 ;
then A53: x2 . i = 1_ FF by ;
not i in J1 by ;
then x1 . i = g . i by ;
then x1 . i = 1_ FF by ;
hence y1 . i = (g +* f) . i by ; :: 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 ;
hence y = g +* f by ; :: 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 ;
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 ;
suppose A60: ( j in J1 & not j in J2 ) ; :: thesis: f . j <> 1_ G
then A61: x1 . j = f1 . j by ;
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 ;
x2 . j = g . j by
.= 1_ G1 by ;
hence f . j <> 1_ G by ; :: thesis: verum
end;
suppose A64: ( not j in J1 & j in J2 ) ; :: thesis: f . j <> 1_ G
then A65: x2 . j = f2 . j by ;
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 ;
x1 . j = g . j by
.= 1_ G2 by ;
hence f . j <> 1_ G by ; :: 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 ;
ex G1 being non empty Group-like multMagma st
( G1 = F . j & f1 . j in the carrier of G1 & f1 . j <> 1_ G1 ) by ;
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 () 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 () || A as BinOp of A by ;
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 b1 being Element of the carrier of multMagma(# A,b #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# A,b #) st
( b1 * b2 = e & b2 * b1 = e ) )

let h be Element of multMagma(# A,b #); :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )

reconsider h1 = h as Element of () by A4;
[h,e] in [:A,A:] by ZFMISC_1:87;
hence h * e = h1 * (1_ ()) by FUNCT_1:49
.= h by GROUP_1:def 4 ;
:: thesis: ( e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )

[e,h] in [:A,A:] by ZFMISC_1:87;
hence e * h = (1_ ()) * h1 by FUNCT_1:49
.= h by GROUP_1:def 4 ;
:: thesis: ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e )

reconsider h2 = h1, hh = h1 " as Element of product () by Def2;
A71: S1[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 S2[ 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 S2[i,j]
proof
let i be object ; :: thesis: ( i in J implies ex j being object st S2[i,j] )
assume A75: i in J ; :: thesis: ex j being object st S2[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 ;
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 ;
then reconsider m = f . i as Element of G by A76;
take m " ; :: thesis: S2[i,m " ]
thus S2[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
S2[j,f9 . j] from 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 . b1 = (g +* f9) . b1 )
assume A81: i in I ; :: thesis: hh . b1 = (g +* f9) . b1
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 ;
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 . b1 = (g +* f9) . b1
then A85: (g +* f9) . i = f9 . i by ;
A86: ex G being Group ex m being Element of G st
( G = F . i & m = f . i & f9 . i = m " ) by ;
h2 . i = f . i by ;
hence hh . i = (g +* f9) . i by A81, A86, A85, Th8; :: thesis: verum
end;
suppose A87: not i in J ; :: thesis: hh . b1 = (g +* f9) . b1
then A88: (g +* f9) . i = g . i by
.= 1_ G3 by ;
A89: 1_ G5 = (1_ G5) " by GROUP_1:8;
h2 . i = g . i by
.= 1_ G3 by ;
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 ;
hence h1 " = g +* f9 by ; :: 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 ; :: 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 ;
hence f9 . j <> 1_ G by ; :: thesis: verum
end;
product () = the carrier of () by Def2;
then reconsider h9 = h1 " as Element of multMagma(# A,b #) by ;
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 ;
take H ; :: thesis: for x being object holds
( x in the carrier of H iff ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & 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 () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & 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 () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & 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 () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & 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 S1[x] by A3;
hence ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & 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 (), J being finite Subset of I, f being ManySortedSet of J such that A95: g = 1_ () 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 () . i
let i be object ; :: thesis: ( i in I implies (g +* f) . b1 in () . b1 )
assume A101: i in I ; :: thesis: (g +* f) . b1 in () . b1
then A102: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by PRALG_1:def 13;
per cases ( i in J or not i in J ) ;
suppose A103: i in J ; :: thesis: (g +* f) . b1 in () . b1
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 () . i by ; :: thesis: verum
end;
suppose A104: not i in J ; :: thesis: (g +* f) . b1 in () . b1
consider G being non empty Group-like multMagma such that
A105: G = F . i by ;
(g +* f) . i = g . i by
.= 1_ G by ;
hence (g +* f) . i in () . i by ; :: thesis: verum
end;
end;
end;
dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1
.= I by ;
then x in product () by ;
hence x in the carrier of H by A3, A95, A96, A97; :: thesis: verum