set A = product (Carrier F);
A1:
dom (Carrier F) = I
by PBOOLE:def 3;
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) );
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[
set ,
set ]
means ex
Fi being non
empty multMagma st
(
Fi = F . $1 & $2
= the
multF of
Fi . (x . $1),
(y . $1) );
A3:
for
i being
set st
i in I holds
ex
w being
set st
(
w in union (rng (Carrier F)) &
S2[
i,
w] )
proof
let i be
set ;
:: thesis: ( i in I implies ex w being set st
( w in union (rng (Carrier F)) & S2[i,w] ) )
assume A4:
i in I
;
:: thesis: ex w being set 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
HGrStr-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:
ex
R being
1-sorted st
(
R = F . i1 &
(Carrier F1) . i1 = the
carrier of
R )
by PRALG_1:def 13;
then
(
x . i1 in the
carrier of
(F1 . i1) &
y . i1 in the
carrier of
(F1 . i1) )
by A1, CARD_3:18;
then A6:
the
multF of
(F1 . i1) . (x . i1),
(y . i1) in the
carrier of
(F1 . i1)
by BINOP_1:29;
(Carrier F) . i1 in rng (Carrier F)
by A1, FUNCT_1:def 5;
hence
w in union (rng (Carrier F))
by A5, A6, TARSKI:def 4;
:: thesis: S2[i,w]
thus
S2[
i,
w]
;
:: thesis: verum
end;
consider z being
Function such that A7:
(
dom z = I &
rng z c= union (rng (Carrier F)) & ( for
x being
set st
x in I holds
S2[
x,
z . x] ) )
from WELLORD2:sch 1(A3);
A8:
dom z = dom (Carrier F)
by A7, PBOOLE:def 3;
for
i being
set st
i in dom (Carrier F) holds
z . i in (Carrier F) . i
proof
let i be
set ;
:: thesis: ( i in dom (Carrier F) implies z . i in (Carrier F) . i )
assume A9:
i in dom (Carrier F)
;
:: thesis: z . i in (Carrier F) . i
then A10:
ex
Fi being non
empty multMagma st
(
Fi = F . i &
z . i = the
multF of
Fi . (x . i),
(y . i) )
by A1, A7;
A11:
ex
R being
1-sorted st
(
R = F . i &
(Carrier F) . i = the
carrier of
R )
by A1, A9, PRALG_1:def 13;
reconsider I1 =
I as non
empty set by A9, PBOOLE:def 3;
reconsider i1 =
i as
Element of
I1 by A9, PBOOLE:def 3;
reconsider F1 =
F as
HGrStr-Family of
I1 ;
(
x . i1 in the
carrier of
(F1 . i1) &
y . i1 in the
carrier of
(F1 . i1) )
by A1, A11, CARD_3:18;
hence
z . i in (Carrier F) . i
by A10, A11, BINOP_1:29;
:: thesis: verum
end;
then reconsider z =
z as
Element of
product (Carrier F) by A8, CARD_3:18;
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 A12:
(
Fi = F . i &
z . i = the
multF of
Fi . (x . i),
(y . i) )
by A7;
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 A12;
:: thesis: verum
end;
consider B being BinOp of product (Carrier F) such that
A13:
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 A13; :: thesis: verum