set A = product (Carrier F);

defpred S_{1}[ Element of product (Carrier F), Element of product (Carrier F), set ] means for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = $3 & h . i = the multF of Fi . (($1 . i),($2 . i)) );

A1: dom (Carrier F) = I by PARTFUN1:def 2;

A2: for x, y being Element of product (Carrier F) ex z being Element of product (Carrier F) st S_{1}[x,y,z]

A16: for a, b being Element of product (Carrier F) holds S_{1}[a,b,B . (a,b)]
from BINOP_1:sch 3(A2);

take multMagma(# (product (Carrier F)),B #) ; :: thesis: ( the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )

thus the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) ; :: thesis: for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

let f, g be Element of product (Carrier F); :: thesis: for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

let i be set ; :: thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) )

assume i in I ; :: thesis: ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

hence ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A16; :: thesis: verum

defpred S

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = $3 & h . i = the multF of Fi . (($1 . i),($2 . i)) );

A1: dom (Carrier F) = I by PARTFUN1:def 2;

A2: for x, y being Element of product (Carrier F) ex z being Element of product (Carrier F) st S

proof

consider B being BinOp of (product (Carrier F)) such that
let x, y be Element of product (Carrier F); :: thesis: ex z being Element of product (Carrier F) st S_{1}[x,y,z]

defpred S_{2}[ object , object ] means ex Fi being non empty multMagma st

( Fi = F . $1 & $2 = the multF of Fi . ((x . $1),(y . $1)) );

A3: for i being object st i in I holds

ex w being object st

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

A8: ( dom z = I & rng z c= union (rng (Carrier F)) & ( for x being object st x in I holds

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

A9: for i being object st i in dom (Carrier F) holds

z . i in (Carrier F) . i

then reconsider z = z as Element of product (Carrier F) by A9, CARD_3:9;

take z ; :: thesis: S_{1}[x,y,z]

let i be set ; :: thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) )

assume i in I ; :: thesis: ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )

then consider Fi being non empty multMagma such that

A14: Fi = F . i and

A15: z . i = the multF of Fi . ((x . i),(y . i)) by A8;

take Fi ; :: thesis: ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )

take z ; :: thesis: ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) )

thus ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) ) by A14, A15; :: thesis: verum

end;defpred S

( Fi = F . $1 & $2 = the multF of Fi . ((x . $1),(y . $1)) );

A3: for i being object st i in I holds

ex w being object st

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

proof

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

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

assume A4: i in I ; :: thesis: ex w being object st

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

then reconsider I1 = I as non empty set ;

reconsider i1 = i as Element of I1 by A4;

reconsider F1 = F as multMagma-Family of I1 ;

take w = the multF of (F1 . i1) . ((x . i1),(y . i1)); :: thesis: ( w in union (rng (Carrier F)) & S_{2}[i,w] )

A5: (Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def 3;

A6: ex R being 1-sorted st

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

then A7: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;

x . i1 in the carrier of (F1 . i1) by A1, A6, CARD_3:9;

then the multF of (F1 . i1) . ((x . i1),(y . i1)) in the carrier of (F1 . i1) by A7, BINOP_1:17;

hence w in union (rng (Carrier F)) by A6, A5, TARSKI:def 4; :: thesis: S_{2}[i,w]

thus S_{2}[i,w]
; :: thesis: verum

end;( w in union (rng (Carrier F)) & S

assume A4: i in I ; :: thesis: ex w being object st

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

then reconsider I1 = I as non empty set ;

reconsider i1 = i as Element of I1 by A4;

reconsider F1 = F as multMagma-Family of I1 ;

take w = the multF of (F1 . i1) . ((x . i1),(y . i1)); :: thesis: ( w in union (rng (Carrier F)) & S

A5: (Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def 3;

A6: ex R being 1-sorted st

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

then A7: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;

x . i1 in the carrier of (F1 . i1) by A1, A6, CARD_3:9;

then the multF of (F1 . i1) . ((x . i1),(y . i1)) in the carrier of (F1 . i1) by A7, BINOP_1:17;

hence w in union (rng (Carrier F)) by A6, A5, TARSKI:def 4; :: thesis: S

thus S

A8: ( dom z = I & rng z c= union (rng (Carrier F)) & ( for x being object st x in I holds

S

A9: for i being object st i in dom (Carrier F) holds

z . i in (Carrier F) . i

proof

dom z = dom (Carrier F)
by A8, PARTFUN1:def 2;
let i be object ; :: thesis: ( i in dom (Carrier F) implies z . i in (Carrier F) . i )

assume A10: i in dom (Carrier F) ; :: thesis: z . i in (Carrier F) . i

then reconsider I1 = I as non empty set ;

A11: ex Fi being non empty multMagma st

( Fi = F . i & z . i = the multF of Fi . ((x . i),(y . i)) ) by A8, A10;

reconsider i1 = i as Element of I1 by A10;

reconsider F1 = F as multMagma-Family of I1 ;

A12: ex R being 1-sorted st

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

then A13: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;

x . i1 in the carrier of (F1 . i1) by A1, A12, CARD_3:9;

hence z . i in (Carrier F) . i by A11, A12, A13, BINOP_1:17; :: thesis: verum

end;assume A10: i in dom (Carrier F) ; :: thesis: z . i in (Carrier F) . i

then reconsider I1 = I as non empty set ;

A11: ex Fi being non empty multMagma st

( Fi = F . i & z . i = the multF of Fi . ((x . i),(y . i)) ) by A8, A10;

reconsider i1 = i as Element of I1 by A10;

reconsider F1 = F as multMagma-Family of I1 ;

A12: ex R being 1-sorted st

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

then A13: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;

x . i1 in the carrier of (F1 . i1) by A1, A12, CARD_3:9;

hence z . i in (Carrier F) . i by A11, A12, A13, BINOP_1:17; :: thesis: verum

then reconsider z = z as Element of product (Carrier F) by A9, CARD_3:9;

take z ; :: thesis: S

let i be set ; :: thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) )

assume i in I ; :: thesis: ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )

then consider Fi being non empty multMagma such that

A14: Fi = F . i and

A15: z . i = the multF of Fi . ((x . i),(y . i)) by A8;

take Fi ; :: thesis: ex h being Function st

( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )

take z ; :: thesis: ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) )

thus ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) ) by A14, A15; :: thesis: verum

A16: for a, b being Element of product (Carrier F) holds S

take multMagma(# (product (Carrier F)),B #) ; :: thesis: ( the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) & ( for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )

thus the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) ; :: thesis: for f, g being Element of product (Carrier F)

for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

let f, g be Element of product (Carrier F); :: thesis: for i being set st i in I holds

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

let i be set ; :: thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) )

assume i in I ; :: thesis: ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

hence ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A16; :: thesis: verum