defpred S_{1}[ 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_{1}[i,y] )

A6: dom ee = I and

rng ee c= union (rng (Carrier F)) and

A7: for x being object st x in I holds

S_{1}[x,ee . x]
from FUNCT_1:sch 6(A2);

then reconsider e1 = ee as Element of (product F) by Def2;

take e1 ; :: according to GROUP_1:def 2 :: thesis: for b_{1} being Element of the carrier of (product F) holds

( b_{1} * e1 = b_{1} & e1 * b_{1} = b_{1} & ex b_{2} being Element of the carrier of (product F) st

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

let h be Element of (product F); :: thesis: ( h * e1 = h & e1 * h = h & ex b_{1} being Element of the carrier of (product F) st

( h * b_{1} = e1 & b_{1} * 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;

hence h * e1 = h by A11, A12; :: thesis: ( e1 * h = h & ex b_{1} being Element of the carrier of (product F) st

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

_{2}[ 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_{2}[i,y] )

A32: dom gg = I and

rng gg c= union (rng (Carrier F)) and

A33: for x being object st x in I holds

S_{2}[x,gg . x]
from FUNCT_1:sch 6(A24);

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_{1} being Element of the carrier of (product F) st

( h * b_{1} = e1 & b_{1} * 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;

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

( 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

proof

consider ee being Function such that
let i be object ; :: thesis: ( i in I implies ex y being object st

( y in union (rng (Carrier F)) & S_{1}[i,y] ) )

assume A3: i in I ; :: thesis: ex y being object st

( y in union (rng (Carrier F)) & S_{1}[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_{1}[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_{1}[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;( y in union (rng (Carrier F)) & S

assume A3: i in I ; :: thesis: ex y being object st

( y in union (rng (Carrier F)) & S

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

(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

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

A6: dom ee = I and

rng ee c= union (rng (Carrier F)) and

A7: for x being object st x in I holds

S

now :: thesis: for i being object st i in dom ee holds

ee . i in (Carrier F) . i

then A10:
ee in product (Carrier F)
by A1, A6, CARD_3:9;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;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

then reconsider e1 = ee as Element of (product F) by Def2;

take e1 ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

let h be Element of (product F); :: thesis: ( h * e1 = h & e1 * h = h & ex b

( h * b

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

dom he = I
by A1, CARD_3:9;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;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

hence h * e1 = h by A11, A12; :: thesis: ( e1 * h = h & ex b

( h * b

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

eh . i = h1 . i

defpred Seh . 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;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

( 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

proof

consider gg being Function such that
let i be object ; :: thesis: ( i in I implies ex y being object st

( y in union (rng (Carrier F)) & S_{2}[i,y] ) )

assume A25: i in I ; :: thesis: ex y being object st

( y in union (rng (Carrier F)) & S_{2}[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_{2}[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_{2}[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;( y in union (rng (Carrier F)) & S

assume A25: i in I ; :: thesis: ex y being object st

( y in union (rng (Carrier F)) & S

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

(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

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

A32: dom gg = I and

rng gg c= union (rng (Carrier F)) and

A33: for x being object st x in I holds

S

now :: thesis: for i being object st i in dom gg holds

gg . i in (Carrier F) . i

then A36:
gg in product (Carrier F)
by A1, A32, CARD_3:9;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;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

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

( h * b

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

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

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

eh . i = ee . i

dom he = I
by A1, CARD_3:9;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;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

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