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_{1}[ 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_{1}[x] ) )
from XBOOLE_0:sch 1();

A4: A c= the carrier of (product F)_{1}[g]

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 )

set H = multMagma(# A,b #);

multMagma(# A,b #) is Group-like

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

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;

.= 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

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

( $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

A4: A c= the carrier of (product F)

proof

A5:
S
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;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

proof

then reconsider A = A as non empty set by A3;
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;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

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

then reconsider b = the multF of (product F) || A as BinOp of A by FUNCT_2:def 1, RELSET_1:4;
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;

.= 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_{2}[ 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_{2}[k] ) )
from XBOOLE_0:sch 1();

A35: S_{1}[y]

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

A24:
dom f2 = J2
by PARTFUN1:def 2;x1 . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies x1 . b_{1} in (Carrier F) . b_{1} )

assume A19: i in I ; :: thesis: x1 . b_{1} in (Carrier F) . b_{1}

then A20: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

end;assume A19: i in I ; :: thesis: x1 . b

then A20: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

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

end;

A25: now :: thesis: for i being object st i in I holds

x2 . i in (Carrier F) . i

A31: dom x1 =
(dom g) \/ (dom f1)
by A13, FUNCT_4:def 1
x2 . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies x2 . b_{1} in (Carrier F) . b_{1} )

assume A26: i in I ; :: thesis: x2 . b_{1} in (Carrier F) . b_{1}

then A27: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

end;assume A26: i in I ; :: thesis: x2 . b

then A27: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

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

end;

.= 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

( 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

A35: S

proof

reconsider ff = X1 * X2 as Element of product (Carrier F) by Def2;
defpred S_{3}[ 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_{3}[j,t]

A40: for j being object st j in J holds

S_{3}[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;

.= 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;

end;( 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

proof

consider f being ManySortedSet of J such that
let j be object ; :: thesis: ( j in J implies ex t being object st S_{3}[j,t] )

assume A38: j in J ; :: thesis: ex t being object st S_{3}[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_{3}[j,k1 * k2]

thus S_{3}[j,k1 * k2]
by A39; :: thesis: verum

end;assume A38: j in J ; :: thesis: ex t being object st S

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

thus S

A40: for j being object st j in J holds

S

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

dom (g +* f) =
(dom g) \/ (dom f)
by FUNCT_4:def 1
y1 . i = (g +* f) . i

let i be object ; :: thesis: ( i in I implies y1 . b_{1} = (g +* f) . b_{1} )

assume A43: i in I ; :: thesis: y1 . b_{1} = (g +* f) . b_{1}

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;

end;assume A43: i in I ; :: thesis: y1 . 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 )
;

end;

suppose A49:
i in J
; :: thesis: y1 . b_{1} = (g +* f) . b_{1}

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;( 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

suppose A50:
not i in J
; :: thesis: y1 . b_{1} = (g +* f) . b_{1}

then A51: (g +* f) . i =
g . i
by A41, FUNCT_4:11

.= 1_ FF by A43, A47, Th6 ;

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

hence
y1 . i = (g +* f) . i
; :: thesis: verumper cases
( not i in J1 \/ J2 or i in K )
by A50, XBOOLE_0:def 5;

end;

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;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

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;( 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

.= 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;

end;

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;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

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;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

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;( 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

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 )

hence
y in A
by A3, A33, A35; :: thesis: verumfor 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;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

set H = multMagma(# A,b #);

multMagma(# A,b #) is Group-like

proof

then reconsider H = multMagma(# A,b #) as non empty Group-like multMagma ;
reconsider e = g as Element of multMagma(# A,b #) by A3, A5;

take e ; :: according to GROUP_1:def 2 :: thesis: for b_{1} being Element of the carrier of multMagma(# A,b #) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of multMagma(# A,b #) st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

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

( h * b_{1} = e & b_{1} * 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_{1} being Element of the carrier of multMagma(# A,b #) st

( h * b_{1} = e & b_{1} * 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_{1} being Element of the carrier of multMagma(# A,b #) st

( h * b_{1} = e & b_{1} * h = e )

reconsider h2 = h1, hh = h1 " as Element of product (Carrier F) by Def2;

A71: S_{1}[h1 " ]

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;take e ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

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

( h * b

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

( h * b

[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

( h * b

reconsider h2 = h1, hh = h1 " as Element of product (Carrier F) by Def2;

A71: S

proof

product (Carrier F) = the carrier of (product F)
by Def2;
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_{2}[ 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_{2}[i,j]

A77: for j being object st j in J holds

S_{2}[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;

( 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;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

( G = F . $1 & m = f . $1 & $2 = m " );

A74: for i being object st i in J holds

ex j being object st S

proof

consider f9 being ManySortedSet of J such that
let i be object ; :: thesis: ( i in J implies ex j being object st S_{2}[i,j] )

assume A75: i in J ; :: thesis: ex j being object st S_{2}[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_{2}[i,m " ]

thus S_{2}[i,m " ]
by A76; :: thesis: verum

end;assume A75: i in J ; :: thesis: ex j being object st S

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

thus S

A77: for j being object st j in J holds

S

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

take
J
; :: thesis: ex f being ManySortedSet of J st hh . i = (g +* f9) . i

let i be object ; :: thesis: ( i in I implies hh . b_{1} = (g +* f9) . b_{1} )

assume A81: i in I ; :: thesis: hh . b_{1} = (g +* f9) . b_{1}

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;

end;assume A81: i in I ; :: thesis: hh . 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 )
;

end;

suppose A84:
i in J
; :: thesis: hh . b_{1} = (g +* f9) . b_{1}

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;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

suppose A87:
not i in J
; :: thesis: hh . b_{1} = (g +* f9) . b_{1}

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;.= 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

( 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

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

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 )

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 ( 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_{1}[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;( 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

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

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

dom (g +* f) =
(dom g) \/ (dom f)
by FUNCT_4:def 1
(g +* f) . i in (Carrier F) . i

let i be object ; :: thesis: ( i in I implies (g +* f) . b_{1} in (Carrier F) . b_{1} )

assume A101: i in I ; :: thesis: (g +* f) . b_{1} in (Carrier F) . b_{1}

then A102: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

end;assume A101: i in I ; :: thesis: (g +* f) . b

then A102: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

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

end;

suppose A103:
i in J
; :: thesis: (g +* f) . b_{1} in (Carrier F) . b_{1}

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;( 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

suppose A104:
not i in J
; :: thesis: (g +* f) . b_{1} in (Carrier F) . b_{1}

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;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

.= 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