reconsider Z = (Bags n) --> (0. L) as Function of (Bags n),the carrier of L ;
defpred S1[ set , set , set ] means ex p, q, r being Polynomial of n,L st
( p = $1 & q = $2 & r = $3 & p *' q = r );
defpred S2[ set , set , set ] means ex p, q, r being Polynomial of n,L st
( p = $1 & q = $2 & r = $3 & p + q = r );
consider x' being finite-Support Series of n,L;
defpred S3[ set ] means ex x' being Series of n,L st
( x' = $1 & x' is finite-Support );
consider P being Subset of (Funcs (Bags n),the carrier of L) such that
A1:
for x being Element of Funcs (Bags n),the carrier of L holds
( x in P iff S3[x] )
from SUBSET_1:sch 3();
x' in Funcs (Bags n),the carrier of L
by FUNCT_2:11;
then reconsider P = P as non empty Subset of (Funcs (Bags n),the carrier of L) by A1;
A2:
now let x,
y be
Element of
P;
:: thesis: ex u being Element of P st S2[x,y,u]reconsider p =
x,
q =
y as
Element of
Funcs (Bags n),the
carrier of
L ;
consider p' being
Series of
n,
L such that A3:
p' = p
and A4:
p' is
finite-Support
by A1;
consider q' being
Series of
n,
L such that A5:
q' = q
and A6:
q' is
finite-Support
by A1;
reconsider p' =
p',
q' =
q' as
Polynomial of
n,
L by A4, A6;
set r =
p' + q';
p' + q' in Funcs (Bags n),the
carrier of
L
by FUNCT_2:11;
then reconsider u =
p' + q' as
Element of
P by A1;
take u =
u;
:: thesis: S2[x,y,u]thus
S2[
x,
y,
u]
by A3, A5;
:: thesis: verum end;
consider fadd being Function of [:P,P:],P such that
A7:
for x, y being Element of P holds S2[x,y,fadd . x,y]
from BINOP_1:sch 3(A2);
A8:
now let x,
y be
Element of
P;
:: thesis: ex u being Element of P st S1[x,y,u]reconsider p =
x,
q =
y as
Element of
Funcs (Bags n),the
carrier of
L ;
consider p' being
Series of
n,
L such that A9:
p' = p
and A10:
p' is
finite-Support
by A1;
consider q' being
Series of
n,
L such that A11:
q' = q
and A12:
q' is
finite-Support
by A1;
reconsider p' =
p',
q' =
q' as
Polynomial of
n,
L by A10, A12;
set r =
p' *' q';
p' *' q' in Funcs (Bags n),the
carrier of
L
by FUNCT_2:11;
then reconsider u =
p' *' q' as
Element of
P by A1;
take u =
u;
:: thesis: S1[x,y,u]thus
S1[
x,
y,
u]
by A9, A11;
:: thesis: verum end;
consider fmult being Function of [:P,P:],P such that
A13:
for x, y being Element of P holds S1[x,y,fmult . x,y]
from BINOP_1:sch 3(A8);
reconsider ZZ = Z as Element of Funcs (Bags n),the carrier of L by FUNCT_2:11;
reconsider Z' = Z as Function of (Bags n),L ;
reconsider Z' = Z' as Series of n,L ;
then
Support Z' = {}
by XBOOLE_0:def 1;
then
Z' is finite-Support
by Def10;
then
ZZ in P
by A1;
then reconsider Ze = Z as Element of P ;
reconsider O = Z +* (EmptyBag n),(1. L) as Function of (Bags n),the carrier of L ;
reconsider O' = O as Function of (Bags n),L ;
reconsider O' = O' as Series of n,L ;
reconsider O = O as Element of Funcs (Bags n),the carrier of L by FUNCT_2:11;
then
Support O' = {(EmptyBag n)}
by TARSKI:def 1;
then
O' is finite-Support
by Def10;
then reconsider O = O as Element of P by A1;
reconsider R = doubleLoopStr(# P,fadd,fmult,O,Ze #) as non empty strict doubleLoopStr ;
take
R
; :: thesis: ( ( for x being set holds
( x in the carrier of R iff x is Polynomial of n,L ) ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. R = 0_ n,L & 1. R = 1_ n,L )
thus
for x being set holds
( x in the carrier of R iff x is Polynomial of n,L )
:: thesis: ( ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. R = 0_ n,L & 1. R = 1_ n,L )
thus
0. R = 0_ n,L
; :: thesis: 1. R = 1_ n,L
thus
1. R = 1_ n,L
; :: thesis: verum