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 :: thesis: ( p is ConstPoly of X,L implies ex a being Element of L st p = a | (X,L) )
assume A1: p is ConstPoly of X,L ; :: thesis: ex a being Element of L st p = a | (X,L)
now :: thesis: ( ( p = 0_ (X,L) & ex a being Element of L st p = a | (X,L) ) or ( Support p = {()} & ex a being Element of L st p = a | (X,L) ) )
per cases ( p = 0_ (X,L) or Support p = {()} ) by ;
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 = {()} ; :: thesis: ex a being Element of L st p = a | (X,L)
set q = (0_ (X,L)) +* ((),(p . ()));
A3: now :: thesis: for x being object st x in Bags X holds
p . x = ((0_ (X,L)) +* ((),(p . ()))) . x
let x be object ; :: thesis: ( x in Bags X implies p . x = ((0_ (X,L)) +* ((),(p . ()))) . x )
assume x in Bags X ; :: thesis: p . x = ((0_ (X,L)) +* ((),(p . ()))) . x
then reconsider x9 = x as bag of X ;
A4: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then A5: (0_ (X,L)) +* ((),(p . ())) = (0_ (X,L)) +* (() .--> (p . ())) by FUNCT_7:def 3;
A6: EmptyBag X in dom (() .--> (p . ())) by TARSKI:def 1;
A7: ((0_ (X,L)) +* ((),(p . ()))) . () = ((0_ (X,L)) +* (() .--> (p . ()))) . () by
.= (() .--> (p . ())) . () by
.= p . () by FUNCOP_1:72 ;
now :: thesis: ( ( x9 = EmptyBag X & p . x = ((0_ (X,L)) +* ((),(p . ()))) . x ) or ( x9 <> EmptyBag X & p . x = ((0_ (X,L)) +* ((),(p . ()))) . x ) )
per cases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;
case x9 = EmptyBag X ; :: thesis: p . x = ((0_ (X,L)) +* ((),(p . ()))) . x
hence p . x = ((0_ (X,L)) +* ((),(p . ()))) . x by A7; :: thesis: verum
end;
case A8: x9 <> EmptyBag X ; :: thesis: p . x = ((0_ (X,L)) +* ((),(p . ()))) . x
A9: x9 is Element of Bags X by PRE_POLY:def 12;
not x9 in Support p by ;
then A10: p . x9 = 0. L by ;
not x9 in dom (() .--> (p . ())) by ;
then ((0_ (X,L)) +* ((),(p . ()))) . x9 = (0_ (X,L)) . x9 by ;
hence p . x = ((0_ (X,L)) +* ((),(p . ()))) . x by ; :: thesis: verum
end;
end;
end;
hence p . x = ((0_ (X,L)) +* ((),(p . ()))) . x ; :: thesis: verum
end;
A11: Bags X = dom ((0_ (X,L)) +* ((),(p . ()))) by FUNCT_2:def 1;
( (0_ (X,L)) +* ((),(p . ())) = (p . ()) | (X,L) & Bags X = dom p ) by FUNCT_2:def 1;
hence ex a being Element of L st p = a | (X,L) by ; :: 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