defpred S₁[ 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 S₁[x] ) from SUBSET_1:sch 3();
consider x' being finite-Support Series of n,L;
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;
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 );

A2: now

let x, y be Element of P; :: thesis:
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 & p' is finite-Support ) by A1;
consider q' being Series of n,L such that
A4: ( q' = q & q' is finite-Support ) by A1;
reconsider p' = p', q' = q' as Polynomial of n,L by A3, A4;
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:
thus S₂[x,y,u] by A3, A4; :: thesis:

end;

consider fadd being Function of [:P,P:],P such that
A5: for x, y being Element of P holds S₂[x,y,fadd . x,y] from BINOP_1:sch 3(A2);
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 );

A6: now

let x, y be Element of P; :: thesis:
reconsider p = x, q = y as Element of Funcs (Bags n),the carrier of L ;
consider p' being Series of n,L such that
A7: ( p' = p & p' is finite-Support ) by A1;
consider q' being Series of n,L such that
A8: ( q' = q & q' is finite-Support ) by A1;
reconsider p' = p', q' = q' as Polynomial of n,L by A7, A8;
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:
thus S₃[x,y,u] by A7, A8; :: thesis:

end;

consider fmult being Function of [:P,P:],P such that
A9: for x, y being Element of P holds S₃[x,y,fmult . x,y] from BINOP_1:sch 3(A6);
reconsider Z = (Bags n) --> (0. L) as Function of (Bags n),the carrier of L ;
reconsider Z' = Z as Function of (Bags n),L ;
reconsider Z' = Z' as Series of n,L ;
reconsider ZZ = Z as Element of Funcs (Bags n),the carrier of L by FUNCT_2:11;

now

given x being set such that A10: x in Support Z' ; :: thesis:
reconsider x = x as Element of Bags n by A10;
Z' . x = 0. L by FUNCOP_1:13;
hence contradiction by A10, Def9; :: thesis:

end;

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;

now

let x be set ; :: thesis:

hereby :: thesis:

assume A11: x in Support O' ; :: thesis:
then reconsider x' = x as Element of Bags n ;
assume x <> EmptyBag n ; :: thesis:
then O' . x = Z . x' by FUNCT_7:34
.= 0. L by FUNCOP_1:13 ;
hence contradiction by A11, Def9; :: thesis:

end;

assume A12: x = EmptyBag n ; :: thesis:
dom Z = Bags n by FUNCOP_1:19;
then O' . x <> 0. L by A12, Th27, FUNCT_7:33;
hence x in Support O' by A12, Def9; :: thesis:

end;

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:
thus for x being set holds
( x in the carrier of R iff x is Polynomial of n,L ) :: thesis:

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A13: x in the carrier of R ; :: thesis:
then reconsider xx = x as Element of Funcs (Bags n),the carrier of L ;
consider x' being Series of n,L such that
A14: ( x' = xx & x' is finite-Support ) by A1, A13;
thus x is Polynomial of n,L by A14; :: thesis:

end;

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

end;

hereby :: thesis:

let x, y be Element of R; :: thesis:
let p, q be Polynomial of n,L; :: thesis:
assume A16: ( x = p & y = q ) ; :: thesis:
consider p', q', r' being Polynomial of n,L such that
A17: ( p' = x & q' = y & r' = fadd . x,y ) and
A18: p' + q' = r' by A5;
thus x + y = p + q by A16, A17, A18; :: thesis:

end;

hereby :: thesis:

let x, y be Element of R; :: thesis:
let p, q be Polynomial of n,L; :: thesis:
assume A19: ( x = p & y = q ) ; :: thesis:
consider p', q', r' being Polynomial of n,L such that
A20: ( p' = x & q' = y & r' = fmult . x,y ) and
A21: p' *' q' = r' by A9;
thus x * y = p *' q by A19, A20, A21; :: thesis:

end;

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