set A = product (Carrier F);
defpred S1[ 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 S1[x,y,z]
proof
let x, y be Element of product (Carrier F); :: thesis: ex z being Element of product (Carrier F) st S1[x,y,z]
defpred S2[ 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)) & S2[i,w] )
proof
let i be object ; :: thesis: ( i in I implies ex w being object st
( w in union (rng (Carrier F)) & S2[i,w] ) )
assume A4: i in I ; :: thesis: ex w being object st
( w in union (rng (Carrier F)) & S2[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)) & S2[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 15;
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: S2[i,w]
thus S2[i,w] ; :: thesis: verum
end;
consider z being Function such that
A8: ( dom z = I & rng z c= union (rng (Carrier F)) & ( for x being object st x in I holds
S2[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
proof
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 15;
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;
dom z = dom (Carrier F) by A8, PARTFUN1:def 2;
then reconsider z = z as Element of product (Carrier F) by A9, CARD_3:9;
take z ; :: thesis: S1[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;
consider B being BinOp of (product (Carrier F)) such that
A16: for a, b being Element of product (Carrier F) holds S1[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