A1:
0_. L in { x where x is Polynomial of L : verum }
;
then reconsider Ca = { x where x is Polynomial of L : verum } as non empty set ;
reconsider Ze = 0_. L as Element of Ca by A1;
defpred S1[ set , set , set ] means ex p, q being Polynomial of L st
( p = $1 & q = $2 & $3 = p + q );
A2:
for x, y being Element of Ca ex u being Element of Ca st S1[x,y,u]
proof
let x,
y be
Element of
Ca;
ex u being Element of Ca st S1[x,y,u]
x in Ca
;
then consider p being
Polynomial of
L such that A3:
x = p
;
y in Ca
;
then consider q being
Polynomial of
L such that A4:
y = q
;
p + q in Ca
;
then reconsider u =
p + q as
Element of
Ca ;
take
u
;
S1[x,y,u]
take
p
;
ex q being Polynomial of L st
( p = x & q = y & u = p + q )
take
q
;
( p = x & q = y & u = p + q )
thus
(
p = x &
q = y &
u = p + q )
by A3, A4;
verum
end;
consider Ad being Function of [:Ca,Ca:],Ca such that
A5:
for x, y being Element of Ca holds S1[x,y,Ad . (x,y)]
from BINOP_1:sch 3(A2);
1_. L in { x where x is Polynomial of L : verum }
;
then reconsider Un = 1_. L as Element of Ca ;
defpred S2[ set , set , set ] means ex p, q being Polynomial of L st
( p = $1 & q = $2 & $3 = p *' q );
A6:
for x, y being Element of Ca ex u being Element of Ca st S2[x,y,u]
proof
let x,
y be
Element of
Ca;
ex u being Element of Ca st S2[x,y,u]
x in Ca
;
then consider p being
Polynomial of
L such that A7:
x = p
;
y in Ca
;
then consider q being
Polynomial of
L such that A8:
y = q
;
p *' q in Ca
;
then reconsider u =
p *' q as
Element of
Ca ;
take
u
;
S2[x,y,u]
take
p
;
ex q being Polynomial of L st
( p = x & q = y & u = p *' q )
take
q
;
( p = x & q = y & u = p *' q )
thus
(
p = x &
q = y &
u = p *' q )
by A7, A8;
verum
end;
consider Mu being Function of [:Ca,Ca:],Ca such that
A9:
for x, y being Element of Ca holds S2[x,y,Mu . (x,y)]
from BINOP_1:sch 3(A6);
reconsider P = doubleLoopStr(# Ca,Ad,Mu,Un,Ze #) as non empty strict doubleLoopStr ;
take
P
; ( ( for x being set holds
( x in the carrier of P iff x is Polynomial of L ) ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )
thus
for x being set holds
( x in the carrier of P iff x is Polynomial of L )
( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )
thus
for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q
( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. P = 0_. L & 1. P = 1_. L )proof
let x,
y be
Element of
P;
for p, q being sequence of L st x = p & y = q holds
x + y = p + qlet p,
q be
sequence of
L;
( x = p & y = q implies x + y = p + q )
assume A10:
(
x = p &
y = q )
;
x + y = p + q
ex
p1,
q1 being
Polynomial of
L st
(
p1 = x &
q1 = y &
Ad . (
x,
y)
= p1 + q1 )
by A5;
hence
x + y = p + q
by A10;
verum
end;
thus
for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q
( 0. P = 0_. L & 1. P = 1_. L )
thus
0. P = 0_. L
; 1. P = 1_. L
thus
1. P = 1_. L
; verum