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

assume A4: i in I ; :: thesis: ex w being object st
( w in union (rng ()) & 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 ()) & S2[i,w] )
A5: (Carrier F) . i1 in rng () by ;
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 ;
x . i1 in the carrier of (F1 . i1) by ;
then the multF of (F1 . i1) . ((x . i1),(y . i1)) in the carrier of (F1 . i1) by ;
hence w in union (rng ()) by ; :: 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 ()) & ( for x being object st x in I holds
S2[x,z . x] ) ) from A9: for i being object st i in dom () holds
z . i in () . i
proof
let i be object ; :: thesis: ( i in dom () implies z . i in () . i )
assume A10: i in dom () ; :: thesis: z . i in () . 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 ;
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 & () . i = the carrier of R ) by ;
then A13: y . i1 in the carrier of (F1 . i1) by ;
x . i1 in the carrier of (F1 . i1) by ;
hence z . i in () . i by ; :: thesis: verum
end;
dom z = dom () by ;
then reconsider z = z as Element of product () by ;
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 ; :: thesis: verum
end;
consider B being BinOp of (product ()) such that
A16: for a, b being Element of product () holds S1[a,b,B . (a,b)] from take multMagma(# (product ()),B #) ; :: thesis: ( the carrier of multMagma(# (product ()),B #) = product () & ( for f, g being Element of product ()
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 ()),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )

thus the carrier of multMagma(# (product ()),B #) = product () ; :: thesis: for f, g being Element of product ()
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 ()),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )

let f, g be Element of product (); :: 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 ()),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 ()),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 ()),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 ()),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A16; :: thesis: verum