let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for a being Element of F holds
( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F
for a being Element of F holds
( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F ) )
assume K: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F
for a being Element of F holds
( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F )
let p be Polynomial of F; :: thesis: for a being Element of F holds
( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F )
let a be Element of F; :: thesis: ( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F )
set n = card (nonConstantPolys F);

A: now :: thesis: ( p = a | F implies Poly (m,p) = a | ((card (nonConstantPolys F)),F) )

assume AS: p = a | F ; :: thesis: Poly (m,p) = a | ((card (nonConstantPolys F)),F)
set q = a | ((card (nonConstantPolys F)),F);

now :: thesis: for o being object st o in Bags (card (nonConstantPolys F)) holds
(Poly (m,p)) . o = (a | ((card (nonConstantPolys F)),F)) . o

let o be object ; :: thesis: ( o in Bags (card (nonConstantPolys F)) implies (Poly (m,p)) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁ )
assume o in Bags (card (nonConstantPolys F)) ; :: thesis: (Poly (m,p)) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁
then reconsider b = o as bag of card (nonConstantPolys F) ;

per cases ( support b = {} or support b = {m} or ( support b <> {} & support b <> {m} ) ) ;

suppose support b = {} ; :: thesis: (Poly (m,p)) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁

then for i being object st i in card (nonConstantPolys F) holds
b . i = {} by PRE_POLY:def 7;
then D: b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6;
hence (Poly (m,p)) . o = p . 0 by defPg
.= a by AS, Th28
.= (a | ((card (nonConstantPolys F)),F)) . o by D, POLYNOM7:18 ;
:: thesis: verum

end;

suppose D: support b = {m} ; :: thesis: (Poly (m,p)) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁

m in {m} by TARSKI:def 1;
then E: b . m <> 0 by D, PRE_POLY:def 7;
F: b <> EmptyBag (card (nonConstantPolys F)) by D;
thus (Poly (m,p)) . o = p . (b . m) by D, defPg
.= 0. F by AS, E, Th28
.= (a | ((card (nonConstantPolys F)),F)) . o by F, POLYNOM7:18 ; :: thesis: verum

end;

suppose E: ( support b <> {} & support b <> {m} ) ; :: thesis: (Poly (m,p)) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁

then D: b <> EmptyBag (card (nonConstantPolys F)) ;
thus (Poly (m,p)) . o = 0. F by E, defPg
.= (a | ((card (nonConstantPolys F)),F)) . o by D, POLYNOM7:18 ; :: thesis: verum

end;

end;

end;

hence Poly (m,p) = a | ((card (nonConstantPolys F)),F) ; :: thesis: verum

end;

now :: thesis: ( Poly (m,p) = a | ((card (nonConstantPolys F)),F) implies p = a | F )

assume AS: Poly (m,p) = a | ((card (nonConstantPolys F)),F) ; :: thesis: p = a | F

now :: thesis: for o being object st o in NAT holds
p . o = (a | F) . o

let o be object ; :: thesis: ( o in NAT implies p . b₁ = (a | F) . b₁ )
assume o in NAT ; :: thesis: p . b₁ = (a | F) . b₁
then reconsider i = o as Element of NAT ;

per cases ( i = 0 or i <> 0 ) ;

suppose B: i = 0 ; :: thesis: p . b₁ = (a | F) . b₁

then p . i = (Poly (m,p)) . (EmptyBag (card (nonConstantPolys F))) by defPg
.= a by AS, POLYNOM7:18
.= (a | F) . i by B, Th28 ;
hence p . o = (a | F) . o ; :: thesis: verum

end;

suppose C: i <> 0 ; :: thesis: p . b₁ = (a | F) . b₁

for o being object st o in {m} holds
o in card (nonConstantPolys F) by K, TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
set b = (S,i) -bag ;
B: support ((S,i) -bag) = S by C, UPROOTS:8;
then D: (S,i) -bag <> EmptyBag (card (nonConstantPolys F)) ;
m in {m} by TARSKI:def 1;
then p . i = p . (((S,i) -bag) . m) by UPROOTS:7
.= (Poly (m,p)) . ((S,i) -bag) by B, defPg
.= 0. F by D, AS, POLYNOM7:18
.= (a | F) . i by C, Th28 ;
hence p . o = (a | F) . o ; :: thesis: verum

end;

end;

end;

hence p = a | F ; :: thesis: verum

end;

hence ( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F ) by A; :: thesis: verum