defpred S₁[ object , object ] means ex Fi being non empty multMagma ex e being Element of Fi st
( Fi = F . I & F = e & ( for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) ) );
set G = product F;
A1: dom (Carrier F) = I by PARTFUN1:def 2;
A2: for i being object st i in I holds
ex y being object st
( y in union (rng (Carrier F)) & S₁[i,y] )

proof

let i be object ; :: thesis: ( i in I implies ex y being object st
( y in union (rng (Carrier F)) & S₁[i,y] ) )
assume A3: i in I ; :: thesis: ex y being object st
( y in union (rng (Carrier F)) & S₁[i,y] )
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = F as Group-like multMagma-Family of I1 ;
A4: ex R being 1-sorted st
( R = F . i1 & (Carrier F1) . i1 = the carrier of R ) by PRALG_1:def 15;
F1 . i1 is Group-like by Def6;
then consider e being Element of (F1 . i1) such that
A5: for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) ;
take e ; :: thesis: ( e in union (rng (Carrier F)) & S₁[i,e] )
(Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def 3;
hence e in union (rng (Carrier F)) by A4, TARSKI:def 4; :: thesis: S₁[i,e]
take F1 . i1 ; :: thesis: ex e being Element of (F1 . i1) st
( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) ) )
take e ; :: thesis: ( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) ) )
thus ( F1 . i1 = F . i & e = e ) ; :: thesis: for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) )
let h be Element of (F1 . i1); :: thesis: ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) by A5; :: thesis: verum

end;

consider ee being Function such that
A6: dom ee = I and
rng ee c= union (rng (Carrier F)) and
A7: for x being object st x in I holds
S₁[x,ee . x] from FUNCT_1:sch 6(A2);

now :: thesis: for i being object st i in dom ee holds
ee . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom ee implies ee . i in (Carrier F) . i )
assume A8: i in dom ee ; :: thesis: ee . i in (Carrier F) . i
then A9: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A6, PRALG_1:def 15;
ex Fi being non empty multMagma ex e being Element of Fi st
( Fi = F . i & ee . i = e & ( for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) ) ) by A6, A7, A8;
hence ee . i in (Carrier F) . i by A9; :: thesis: verum

end;

then A10: ee in product (Carrier F) by A1, A6, CARD_3:9;
then reconsider e1 = ee as Element of (product F) by Def2;
take e1 ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of (product F) holds
( b₁ * e1 = b₁ & e1 * b₁ = b₁ & ex b₂ being Element of the carrier of (product F) st
( b₁ * b₂ = e1 & b₂ * b₁ = e1 ) )
let h be Element of (product F); :: thesis: ( h * e1 = h & e1 * h = h & ex b₁ being Element of the carrier of (product F) st
( h * b₁ = e1 & b₁ * h = e1 ) )
reconsider h1 = h as Element of product (Carrier F) by Def2;
reconsider he = the multF of (product F) . (h,e1), eh = the multF of (product F) . (e1,h) as Element of product (Carrier F) by Def2;
A11: dom h1 = I by A1, CARD_3:9;

A12: now :: thesis: for i being object st i in I holds
he . i = h1 . i

let i be object ; :: thesis: ( i in I implies he . i = h1 . i )
assume A13: i in I ; :: thesis: he . i = h1 . i
then consider Fi being non empty multMagma , e2 being Element of Fi such that
A14: Fi = F . i and
A15: ee . i = e2 and
A16: for h being Element of Fi holds
( h * e2 = h & e2 * h = h & ex g being Element of Fi st
( h * g = e2 & g * h = e2 ) ) by A7;
reconsider h2 = h1 . i as Element of Fi by A13, A14, Lm1;
A17: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of (product F) . (h1,e1) & f . i = the multF of Gi . ((h1 . i),(ee . i)) ) by A10, A13, Def2;
h2 * e2 = h2 by A16;
hence he . i = h1 . i by A17, A14, A15; :: thesis: verum

end;

dom he = I by A1, CARD_3:9;
hence h * e1 = h by A11, A12; :: thesis: ( e1 * h = h & ex b₁ being Element of the carrier of (product F) st
( h * b₁ = e1 & b₁ * h = e1 ) )

A18: now :: thesis: for i being object st i in I holds
eh . i = h1 . i

let i be object ; :: thesis: ( i in I implies eh . i = h1 . i )
assume A19: i in I ; :: thesis: eh . i = h1 . i
then consider Fi being non empty multMagma , e2 being Element of Fi such that
A20: Fi = F . i and
A21: ee . i = e2 and
A22: for h being Element of Fi holds
( h * e2 = h & e2 * h = h & ex g being Element of Fi st
( h * g = e2 & g * h = e2 ) ) by A7;
reconsider h2 = h1 . i as Element of Fi by A19, A20, Lm1;
A23: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of (product F) . (e1,h1) & f . i = the multF of Gi . ((ee . i),(h1 . i)) ) by A10, A19, Def2;
e2 * h2 = h2 by A22;
hence eh . i = h1 . i by A23, A20, A21; :: thesis: verum

end;

defpred S₂[ object , object ] means ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . I & hi = h1 . I & ex g being Element of Fi st
( hi * g = ee . I & g * hi = ee . I & F = g ) );
A24: for i being object st i in I holds
ex y being object st
( y in union (rng (Carrier F)) & S₂[i,y] )

proof

let i be object ; :: thesis: ( i in I implies ex y being object st
( y in union (rng (Carrier F)) & S₂[i,y] ) )
assume A25: i in I ; :: thesis: ex y being object st
( y in union (rng (Carrier F)) & S₂[i,y] )
then consider Fi being non empty multMagma , e being Element of Fi such that
A26: Fi = F . i and
A27: ee . i = e and
A28: for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) by A7;
A29: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A25, PRALG_1:def 15;
reconsider hi = h1 . i as Element of Fi by A25, A26, Lm1;
consider g being Element of Fi such that
A30: hi * g = e and
A31: g * hi = e by A28;
take g ; :: thesis: ( g in union (rng (Carrier F)) & S₂[i,g] )
(Carrier F) . i in rng (Carrier F) by A1, A25, FUNCT_1:def 3;
hence g in union (rng (Carrier F)) by A26, A29, TARSKI:def 4; :: thesis: S₂[i,g]
take Fi ; :: thesis: ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g ) )
take hi ; :: thesis: ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g ) )
thus ( Fi = F . i & hi = h1 . i ) by A26; :: thesis: ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g )
take g ; :: thesis: ( hi * g = ee . i & g * hi = ee . i & g = g )
thus ( hi * g = ee . i & g * hi = ee . i & g = g ) by A27, A30, A31; :: thesis: verum

end;

consider gg being Function such that
A32: dom gg = I and
rng gg c= union (rng (Carrier F)) and
A33: for x being object st x in I holds
S₂[x,gg . x] from FUNCT_1:sch 6(A24);

now :: thesis: for i being object st i in dom gg holds
gg . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom gg implies gg . i in (Carrier F) . i )
assume A34: i in dom gg ; :: thesis: gg . i in (Carrier F) . i
then A35: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A32, PRALG_1:def 15;
ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A32, A33, A34;
hence gg . i in (Carrier F) . i by A35; :: thesis: verum

end;

then A36: gg in product (Carrier F) by A1, A32, CARD_3:9;
then reconsider g1 = gg as Element of (product F) by Def2;
dom eh = I by A1, CARD_3:9;
hence e1 * h = h by A11, A18; :: thesis: ex b₁ being Element of the carrier of (product F) st
( h * b₁ = e1 & b₁ * h = e1 )
take g1 ; :: thesis: ( h * g1 = e1 & g1 * h = e1 )
reconsider he = the multF of (product F) . (h,g1), eh = the multF of (product F) . (g1,h) as Element of product (Carrier F) by Def2;

A37: now :: thesis: for i being object st i in I holds
he . i = ee . i

let i be object ; :: thesis: ( i in I implies he . i = ee . i )
assume A38: i in I ; :: thesis: he . i = ee . i
then A39: ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33;
ex Gi being non empty multMagma ex h5 being Function st
( Gi = F . i & h5 = the multF of (product F) . (h1,gg) & h5 . i = the multF of Gi . ((h1 . i),(gg . i)) ) by A36, A38, Def2;
hence he . i = ee . i by A39; :: thesis: verum

end;

A40: now :: thesis: for i being object st i in I holds
eh . i = ee . i

let i be object ; :: thesis: ( i in I implies eh . i = ee . i )
assume A41: i in I ; :: thesis: eh . i = ee . i
then A42: ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33;
ex Gi being non empty multMagma ex h5 being Function st
( Gi = F . i & h5 = the multF of (product F) . (gg,h1) & h5 . i = the multF of Gi . ((gg . i),(h1 . i)) ) by A36, A41, Def2;
hence eh . i = ee . i by A42; :: thesis: verum

end;

dom he = I by A1, CARD_3:9;
hence h * g1 = e1 by A6, A37; :: thesis: g1 * h = e1
dom eh = I by A1, CARD_3:9;
hence g1 * h = e1 by A6, A40; :: thesis: verum