defpred S1[ 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 () = I by PARTFUN1:def 2;
A2: for i being object st i in I holds
ex y being object st
( y in union (rng ()) & S1[i,y] )
proof
let i be object ; :: thesis: ( i in I implies ex y being object st
( y in union (rng ()) & S1[i,y] ) )

assume A3: i in I ; :: thesis: ex y being object st
( y in union (rng ()) & S1[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 13;
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 ()) & S1[i,e] )
(Carrier F) . i1 in rng () by ;
hence e in union (rng ()) by ; :: thesis: S1[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 ()) and
A7: for x being object st x in I holds
S1[x,ee . x] from
now :: thesis: for i being object st i in dom ee holds
ee . i in () . i
let i be object ; :: thesis: ( i in dom ee implies ee . i in () . i )
assume A8: i in dom ee ; :: thesis: ee . i in () . i
then A9: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by ;
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 () . i by A9; :: thesis: verum
end;
then A10: ee in product () by ;
then reconsider e1 = ee as Element of () by Def2;
take e1 ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of () holds
( b1 * e1 = b1 & e1 * b1 = b1 & ex b2 being Element of the carrier of () st
( b1 * b2 = e1 & b2 * b1 = e1 ) )

let h be Element of (); :: thesis: ( h * e1 = h & e1 * h = h & ex b1 being Element of the carrier of () st
( h * b1 = e1 & b1 * h = e1 ) )

reconsider h1 = h as Element of product () by Def2;
reconsider he = the multF of () . (h,e1), eh = the multF of () . (e1,h) as Element of product () by Def2;
A11: dom h1 = I by ;
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 ;
A17: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of () . (h1,e1) & f . i = the multF of Gi . ((h1 . i),(ee . i)) ) by ;
h2 * e2 = h2 by A16;
hence he . i = h1 . i by ; :: thesis: verum
end;
dom he = I by ;
hence h * e1 = h by ; :: thesis: ( e1 * h = h & ex b1 being Element of the carrier of () st
( h * b1 = e1 & b1 * 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 ;
A23: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of () . (e1,h1) & f . i = the multF of Gi . ((ee . i),(h1 . i)) ) by ;
e2 * h2 = h2 by A22;
hence eh . i = h1 . i by ; :: thesis: verum
end;
defpred S2[ 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 ()) & S2[i,y] )
proof
let i be object ; :: thesis: ( i in I implies ex y being object st
( y in union (rng ()) & S2[i,y] ) )

assume A25: i in I ; :: thesis: ex y being object st
( y in union (rng ()) & S2[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 & () . i = the carrier of R ) by ;
reconsider hi = h1 . i as Element of Fi by ;
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 ()) & S2[i,g] )
(Carrier F) . i in rng () by ;
hence g in union (rng ()) by ; :: thesis: S2[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 ; :: thesis: verum
end;
consider gg being Function such that
A32: dom gg = I and
rng gg c= union (rng ()) and
A33: for x being object st x in I holds
S2[x,gg . x] from
now :: thesis: for i being object st i in dom gg holds
gg . i in () . i
let i be object ; :: thesis: ( i in dom gg implies gg . i in () . i )
assume A34: i in dom gg ; :: thesis: gg . i in () . i
then A35: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by ;
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 ;
hence gg . i in () . i by A35; :: thesis: verum
end;
then A36: gg in product () by ;
then reconsider g1 = gg as Element of () by Def2;
dom eh = I by ;
hence e1 * h = h by ; :: thesis: ex b1 being Element of the carrier of () st
( h * b1 = e1 & b1 * h = e1 )

take g1 ; :: thesis: ( h * g1 = e1 & g1 * h = e1 )
reconsider he = the multF of () . (h,g1), eh = the multF of () . (g1,h) as Element of product () 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 () . (h1,gg) & h5 . i = the multF of Gi . ((h1 . i),(gg . i)) ) by ;
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 () . (gg,h1) & h5 . i = the multF of Gi . ((gg . i),(h1 . i)) ) by ;
hence eh . i = ee . i by A42; :: thesis: verum
end;
dom he = I by ;
hence h * g1 = e1 by ; :: thesis: g1 * h = e1
dom eh = I by ;
hence g1 * h = e1 by ; :: thesis: verum