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 = {(EmptyBag X)} & ex a being Element of L st p = a | (X,L) ) )
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 :: thesis: for x being object st x in Bags X holds
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 ;
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 ) )
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 A7; :: thesis: verum
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;
end;
end;
hence p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x ; :: thesis: verum
end;
A11: 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 A11, 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