reconsider Z = (Bags n) --> (0. L) as Function of (Bags n), the carrier of L ;
defpred S₁[ set , set , set ] means ex p, q, r being Polynomial of n,L st
( p = $1 & q = $2 & r = $3 & p *' q = r );
defpred S₂[ set , set , set ] means ex p, q, r being Polynomial of n,L st
( p = $1 & q = $2 & r = $3 & p + q = r );
set x9 = the finite-Support Series of n,L;
defpred S₃[ set ] means ex x9 being Series of n,L st
( x9 = $1 & x9 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 S₃[x] ) from SUBSET_1:sch 3();
the finite-Support Series of n,L in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider P = P as non empty Subset of (Funcs ((Bags n), the carrier of L)) by A1;

A2: now :: thesis: for x, y being Element of P ex u being Element of P st S₂[x,y,u]

let x, y be Element of P; :: thesis: ex u being Element of P st S₂[x,y,u]
reconsider p = x, q = y as Element of Funcs ((Bags n), the carrier of L) ;
consider p9 being Series of n,L such that
A3: p9 = p and
A4: p9 is finite-Support by A1;
consider q9 being Series of n,L such that
A5: q9 = q and
A6: q9 is finite-Support by A1;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A4, A6;
set r = p9 + q9;
p9 + q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider u = p9 + q9 as Element of P by A1;
take u = u; :: thesis: S₂[x,y,u]
thus S₂[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 S₂[x,y,fadd . (x,y)] from BINOP_1:sch 3(A2);

A8: now :: thesis: for x, y being Element of P ex u being Element of P st S₁[x,y,u]

let x, y be Element of P; :: thesis: ex u being Element of P st S₁[x,y,u]
reconsider p = x, q = y as Element of Funcs ((Bags n), the carrier of L) ;
consider p9 being Series of n,L such that
A9: p9 = p and
A10: p9 is finite-Support by A1;
consider q9 being Series of n,L such that
A11: q9 = q and
A12: q9 is finite-Support by A1;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A10, A12;
set r = p9 *' q9;
p9 *' q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider u = p9 *' q9 as Element of P by A1;
take u = u; :: thesis: S₁[x,y,u]
thus S₁[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 S₁[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:8;
reconsider Z9 = Z as Function of (Bags n),L ;
reconsider Z9 = Z9 as Series of n,L ;

now :: thesis: for x being object holds not x in Support Z9

given x being object such that A14: x in Support Z9 ; :: thesis: contradiction
reconsider x = x as Element of Bags n by A14;
Z9 . x = 0. L ;
hence contradiction by A14, Def4; :: thesis: verum

end;

then Support Z9 = {} by XBOOLE_0:def 1;
then Z9 is finite-Support ;
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 O9 = O as Function of (Bags n),L ;
reconsider O9 = O9 as Series of n,L ;
reconsider O = O as Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8;

now :: thesis: for x being object holds
( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )

let x be object ; :: thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )

hereby :: thesis: ( x = EmptyBag n implies x in Support O9 )

assume A15: x in Support O9 ; :: thesis: not x <> EmptyBag n
then reconsider x9 = x as Element of Bags n ;
assume x <> EmptyBag n ; :: thesis: contradiction
then O9 . x = Z . x9 by FUNCT_7:32
.= 0. L ;
hence contradiction by A15, Def4; :: thesis: verum

end;

assume A16: x = EmptyBag n ; :: thesis: x in Support O9
dom Z = Bags n ;
then O9 . x <> 0. L by A16, FUNCT_7:31;
hence x in Support O9 by A16, Def4; :: thesis: verum

end;

then Support O9 = {(EmptyBag n)} by TARSKI:def 1;
then O9 is finite-Support ;
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) )

proof

let x be set ; :: thesis: ( x in the carrier of R iff x is Polynomial of n,L )

hereby :: thesis: ( x is Polynomial of n,L implies x in the carrier of R )

assume A17: x in the carrier of R ; :: thesis: x is Polynomial of n,L
then reconsider xx = x as Element of Funcs ((Bags n), the carrier of L) ;
ex x9 being Series of n,L st
( x9 = xx & x9 is finite-Support ) by A1, A17;
hence x is Polynomial of n,L ; :: thesis: verum

end;

assume A18: x is Polynomial of n,L ; :: thesis: x in the carrier of R
then x is Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
hence x in the carrier of R by A1, A18; :: thesis: verum

end;

hereby :: 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 ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )

let x, y be Element of R; :: thesis: for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q
let p, q be Polynomial of n,L; :: thesis: ( x = p & y = q implies x + y = p + q )
assume A19: ( x = p & y = q ) ; :: thesis: x + y = p + q
ex p9, q9, r9 being Polynomial of n,L st
( p9 = x & q9 = y & r9 = fadd . (x,y) & p9 + q9 = r9 ) by A7;
hence x + y = p + q by A19; :: thesis: verum

end;

hereby :: thesis: ( 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )

let x, y be Element of R; :: thesis: for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q
let p, q be Polynomial of n,L; :: thesis: ( x = p & y = q implies x * y = p *' q )
assume A20: ( x = p & y = q ) ; :: thesis: x * y = p *' q
ex p9, q9, r9 being Polynomial of n,L st
( p9 = x & q9 = y & r9 = fmult . (x,y) & p9 *' q9 = r9 ) by A13;
hence x * y = p *' q by A20; :: thesis: verum

end;

thus 0. R = 0_ (n,L) ; :: thesis: 1. R = 1_ (n,L)
thus 1. R = 1_ (n,L) ; :: thesis: verum