let X be set ; :: thesis: for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | X,L )
let L be non empty ZeroStr ; :: thesis: for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | X,L )
let p be Series of X,L; :: thesis: ( p is ConstPoly of X,L iff ex a being Element of L st p = a | X,L )

now

assume A1: p is ConstPoly of X,L ; :: thesis: ex a being Element of L st p = a | X,L

now

per cases ( p = 0_ X,L or Support p = {(EmptyBag X)} ) by A1, Th14;

case p = 0_ X,L ; :: thesis: ex a being Element of L st p = a | X,L

then p = (0. L) | X,L by Lm3;
hence ex a being Element of L st p = a | X,L ; :: thesis: verum

end;

case A2: Support p = {(EmptyBag X)} ; :: thesis: ex a being Element of L st p = a | X,L

set q = (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X));

A3: now

let x be set ; :: thesis: ( x in Bags X implies p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x )
assume x in Bags X ; :: thesis: p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x
then reconsider x9 = x as bag of X ;
A4: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
then A5: (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X)) = (0_ X,L) +* ((EmptyBag X) .--> (p . (EmptyBag X))) by FUNCT_7:def 3;
A6: dom ((EmptyBag X) .--> (p . (EmptyBag X))) = {(EmptyBag X)} by FUNCOP_1:19;
then A7: EmptyBag X in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by TARSKI:def 1;
A8: ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> (p . (EmptyBag X)))) . (EmptyBag X) by A4, FUNCT_7:def 3
.= ((EmptyBag X) .--> (p . (EmptyBag X))) . (EmptyBag X) by A7, FUNCT_4:14
.= p . (EmptyBag X) by FUNCOP_1:87 ;

now

per cases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;

case x9 = EmptyBag X ; :: thesis: p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x

hence p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x by A8; :: thesis: verum

end;

case A9: x9 <> EmptyBag X ; :: thesis: p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x

A10: x9 is Element of Bags X by PRE_POLY:def 12;
not x9 in Support p by A2, A9, TARSKI:def 1;
then A11: p . x9 = 0. L by A10, POLYNOM1:def 9;
not x9 in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by A6, A9, TARSKI:def 1;
then ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x9 = (0_ X,L) . x9 by A5, FUNCT_4:12;
hence p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x by A11, POLYNOM1:81; :: thesis: verum

end;

end;

end;

hence p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x ; :: thesis: verum

end;

A12: Bags X = dom ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) by FUNCT_2:def 1;
( (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X)) = (p . (EmptyBag X)) | X,L & Bags X = dom p ) by FUNCT_2:def 1;
hence ex a being Element of L st p = a | X,L by A12, A3, FUNCT_1:9; :: thesis: verum

end;

end;

end;

hence ex a being Element of L st p = a | X,L ; :: thesis: verum

end;

hence ( p is ConstPoly of X,L iff ex a being Element of L st p = a | X,L ) ; :: thesis: verum