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: (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X)) = (p . (EmptyBag X)) | X,L ;
A4: Bags X = dom p by FUNCT_2:def 1;
A5: Bags X = dom ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) by FUNCT_2:def 1;

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 x' = x as bag of by POLYNOM1:def 14;
A6: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
then A7: (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X)) = (0_ X,L) +* ((EmptyBag X) .--> (p . (EmptyBag X))) by FUNCT_7:def 3;
A8: dom ((EmptyBag X) .--> (p . (EmptyBag X))) = {(EmptyBag X)} by FUNCOP_1:19;
then A9: EmptyBag X in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by TARSKI:def 1;
A10: ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> (p . (EmptyBag X)))) . (EmptyBag X) by A6, FUNCT_7:def 3
.= ((EmptyBag X) .--> (p . (EmptyBag X))) . (EmptyBag X) by A9, FUNCT_4:14
.= p . (EmptyBag X) by FUNCOP_1:87 ;

now

per cases ( x' = EmptyBag X or x' <> EmptyBag X ) ;

case x' = 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 A10; :: thesis: verum

end;

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

then not x' in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by A8, TARSKI:def 1;
then A12: ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x' = (0_ X,L) . x' by A7, FUNCT_4:12;
A13: not x' in Support p by A2, A11, TARSKI:def 1;
x' is Element of Bags X by POLYNOM1:def 14;
then p . x' = 0. L by A13, POLYNOM1:def 9;
hence p . x = ((0_ X,L) +* (EmptyBag X),(p . (EmptyBag X))) . x by A12, POLYNOM1:81; :: thesis: verum

end;

end;

end;

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

end;

then p = (0_ X,L) +* (EmptyBag X),(p . (EmptyBag X)) by A4, A5, FUNCT_1:9;
hence ex a being Element of L st p = a | X,L by A3; :: 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