let X be set ; 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 ; 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; ( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
now ( 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
;
ex a being Element of L st p = a | (X,L)now ( ( 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 A2:
Support p = {(EmptyBag X)}
;
ex a being Element of L st p = a | (X,L)set q =
(0_ (X,L)) +* (
(EmptyBag X),
(p . (EmptyBag X)));
A3:
now for x being object st x in Bags X holds
p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . xlet x be
object ;
( x in Bags X implies p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x )assume
x in Bags X
;
p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . xthen 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 ( ( 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 A8:
x9 <> EmptyBag X
;
p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . xA9:
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;
verum end; end; end; hence
p . x = ((0_ (X,L)) +* ((EmptyBag X),(p . (EmptyBag X)))) . x
;
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;
verum end; end; end; hence
ex
a being
Element of
L st
p = a | (
X,
L)
;
verum end;
hence
( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )
; verum