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) )

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) )

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

end;now :: thesis: ( ( p = 0_ (X,L) & ex a being Element of L st p = a | (X,L) ) or ( Support p = {(EmptyBag X)} & ex a being Element of L st p = a | (X,L) ) )end;

hence
ex a being Element of L st p = a | (X,L)
; :: thesis: verumper cases
( p = 0_ (X,L) or Support p = {(EmptyBag X)} )
by A1, Th14;

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)));

( (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 A11, A3, FUNCT_1:2; :: thesis: verum

end;A3: now :: thesis: for x being object st x in Bags X holds

p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x

A11:
Bags X = dom ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X))))
by FUNCT_2:def 1;p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x

let x be object ; :: 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 8

.= Bags X ;

then A5: (0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X))) = (0_ (X,L)) +* ((EmptyBag X) .--> (p . (EmptyBag X))) by FUNCT_7:def 3;

A6: EmptyBag X in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by TARSKI:def 1;

A7: ((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 A6, FUNCT_4:13

.= p . (EmptyBag X) by FUNCOP_1:72 ;

end;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 8

.= Bags X ;

then A5: (0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X))) = (0_ (X,L)) +* ((EmptyBag X) .--> (p . (EmptyBag X))) by FUNCT_7:def 3;

A6: EmptyBag X in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by TARSKI:def 1;

A7: ((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 A6, FUNCT_4:13

.= p . (EmptyBag X) by FUNCOP_1:72 ;

now :: thesis: ( ( x9 = EmptyBag X & p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x ) or ( x9 <> EmptyBag X & p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x ) )end;

hence
p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x
; :: thesis: verumper cases
( x9 = EmptyBag X or x9 <> EmptyBag X )
;

end;

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

A9:
x9 is Element of Bags X
by PRE_POLY:def 12;

not x9 in Support p by A2, A8, TARSKI:def 1;

then A10: p . x9 = 0. L by A9, POLYNOM1:def 4;

not x9 in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by A8, 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 A10, POLYNOM1:22; :: thesis: verum

end;not x9 in Support p by A2, A8, TARSKI:def 1;

then A10: p . x9 = 0. L by A9, POLYNOM1:def 4;

not x9 in dom ((EmptyBag X) .--> (p . (EmptyBag X))) by A8, 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 A10, POLYNOM1:22; :: thesis: verum

( (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 A11, A3, FUNCT_1:2; :: thesis: verum