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 7
.= Bags X by FUNCOP_1:13 ;
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:13;
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:13
.= p . (EmptyBag X) by FUNCOP_1:72 ;

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 3;
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:11;
hence p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x by A11, POLYNOM1:22; :: 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:2; :: 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