set C = unionCarrier (S,f,E);
defpred S1[ object , object , object ] means ex p being Element of S ex x, y being Element of (p `1) st
( x = $1 & y = $2 & $3 = x * y );
A:
for a, b being Element of unionCarrier (S,f,E) ex z being Element of unionCarrier (S,f,E) st S1[a,b,z]
proof
let a,
b be
Element of
unionCarrier (
S,
f,
E);
ex z being Element of unionCarrier (S,f,E) st S1[a,b,z]
consider Y being
set such that A0:
(
a in Y &
Y in { the carrier of (p `1) where p is Element of S : verum } )
by TARSKI:def 4;
consider pa being
Element of
S such that A1:
Y = the
carrier of
(pa `1)
by A0;
consider Z being
set such that A2:
(
b in Z &
Z in { the carrier of (p `1) where p is Element of S : verum } )
by TARSKI:def 4;
consider pb being
Element of
S such that A3:
Z = the
carrier of
(pb `1)
by A2;
per cases
( pa <= pb or pb <= pa )
by dasc;
suppose
pa <= pb
;
ex z being Element of unionCarrier (S,f,E) st S1[a,b,z]then
pa `1 is
Subfield of
pb `1
by FIELD_4:7;
then
the
carrier of
(pa `1) c= the
carrier of
(pb `1)
by EC_PF_1:def 1;
then reconsider x =
a,
y =
b as
Element of
(pb `1) by A0, A1, A2, A3;
(
x + y in the
carrier of
(pb `1) & the
carrier of
(pb `1) in { the carrier of (p `1) where p is Element of S : verum } )
;
then reconsider z =
x * y as
Element of
unionCarrier (
S,
f,
E)
by TARSKI:def 4;
take
z
;
S1[a,b,z]thus
S1[
a,
b,
z]
;
verum end; suppose
pb <= pa
;
ex z being Element of unionCarrier (S,f,E) st S1[a,b,z]then
pb `1 is
Subfield of
pa `1
by FIELD_4:7;
then
the
carrier of
(pb `1) c= the
carrier of
(pa `1)
by EC_PF_1:def 1;
then reconsider x =
a,
y =
b as
Element of
(pa `1) by A0, A1, A2, A3;
(
x + y in the
carrier of
(pa `1) & the
carrier of
(pa `1) in { the carrier of (p `1) where p is Element of S : verum } )
;
then reconsider z =
x * y as
Element of
unionCarrier (
S,
f,
E)
by TARSKI:def 4;
take
z
;
S1[a,b,z]thus
S1[
a,
b,
z]
;
verum end;
end;
consider A being Function of [:(unionCarrier (S,f,E)),(unionCarrier (S,f,E)):],(unionCarrier (S,f,E)) such that
B:
for x, y being Element of unionCarrier (S,f,E) holds S1[x,y,A . (x,y)]
from BINOP_1:sch 3(A);
reconsider A = A as BinOp of (unionCarrier (S,f,E)) ;
take
A
; for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & A . (a,b) = x * y )
thus
for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & A . (a,b) = x * y )
by B; verum