let F be Field; :: thesis: for m being Ordinal
for a being Element of F holds Poly (m,(a | F)) = a | ((card (nonConstantPolys F)),F)
let m be Ordinal; :: thesis: for a being Element of F holds Poly (m,(a | F)) = a | ((card (nonConstantPolys F)),F)
let a be Element of F; :: thesis: Poly (m,(a | F)) = a | ((card (nonConstantPolys F)),F)
set n = card (nonConstantPolys F);
set pa = Poly (m,(a | F));

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

let o be object ; :: thesis: ( o in Bags (card (nonConstantPolys F)) implies (Poly (m,(a | F))) . b₁ = (a | ((card (nonConstantPolys F)),F)) . b₁ )
assume o in Bags (card (nonConstantPolys F)) ; :: thesis: (Poly (m,(a | F))) . 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,(a | F))) . 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 H: b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6;
then (Poly (m,(a | F))) . b = (a | F) . 0 by defPg
.= a by Th28
.= (a | ((card (nonConstantPolys F)),F)) . b by H, POLYNOM7:18 ;
hence (Poly (m,(a | F))) . o = (a | ((card (nonConstantPolys F)),F)) . o ; :: thesis: verum

end;

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

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

end;

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

then I: b <> EmptyBag (card (nonConstantPolys F)) ;
(Poly (m,(a | F))) . b = 0. F by H, defPg
.= (a | ((card (nonConstantPolys F)),F)) . b by I, POLYNOM7:18 ;
hence (Poly (m,(a | F))) . o = (a | ((card (nonConstantPolys F)),F)) . o ; :: thesis: verum

end;

end;

end;

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