let F be Field; :: thesis: for m being Ordinal
for p, q being Polynomial of F holds Poly (m,(p + q)) = (Poly (m,p)) + (Poly (m,q))
let m be Ordinal; :: thesis: for p, q being Polynomial of F holds Poly (m,(p + q)) = (Poly (m,p)) + (Poly (m,q))
let p, q be Polynomial of F; :: thesis: Poly (m,(p + q)) = (Poly (m,p)) + (Poly (m,q))
set r1 = Poly (m,p);
set r2 = Poly (m,q);
set r = Poly (m,(p + q));
set n = card (nonConstantPolys F);
I: dom (Poly (m,(p + q))) = Bags (card (nonConstantPolys F)) by FUNCT_2:def 1
.= dom ((Poly (m,p)) + (Poly (m,q))) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom (Poly (m,(p + q))) holds
(Poly (m,(p + q))) . o = ((Poly (m,p)) + (Poly (m,q))) . o

let o be object ; :: thesis: ( o in dom (Poly (m,(p + q))) implies (Poly (m,(p + q))) . b₁ = ((Poly (m,p)) + (Poly (m,q))) . b₁ )
assume o in dom (Poly (m,(p + q))) ; :: thesis: (Poly (m,(p + q))) . b₁ = ((Poly (m,p)) + (Poly (m,q))) . 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 + q))) . b₁ = ((Poly (m,p)) + (Poly (m,q))) . 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,(p + q))) . b = (p + q) . 0 by defPg
.= (p . 0) + (q . 0) by NORMSP_1:def 2
.= ((Poly (m,p)) . b) + (q . 0) by H, defPg
.= ((Poly (m,p)) . b) + ((Poly (m,q)) . b) by H, defPg
.= ((Poly (m,p)) + (Poly (m,q))) . b by POLYNOM1:15 ;
hence (Poly (m,(p + q))) . o = ((Poly (m,p)) + (Poly (m,q))) . o ; :: thesis: verum

end;

suppose H: support b = {m} ; :: thesis: (Poly (m,(p + q))) . b₁ = ((Poly (m,p)) + (Poly (m,q))) . b₁

then (Poly (m,(p + q))) . b = (p + q) . (b . m) by defPg
.= (p . (b . m)) + (q . (b . m)) by NORMSP_1:def 2
.= ((Poly (m,p)) . b) + (q . (b . m)) by H, defPg
.= ((Poly (m,p)) . b) + ((Poly (m,q)) . b) by H, defPg
.= ((Poly (m,p)) + (Poly (m,q))) . b by POLYNOM1:15 ;
hence (Poly (m,(p + q))) . o = ((Poly (m,p)) + (Poly (m,q))) . o ; :: thesis: verum

end;

suppose H: ( support b <> {} & support b <> {m} ) ; :: thesis: (Poly (m,(p + q))) . b₁ = ((Poly (m,p)) + (Poly (m,q))) . b₁

then (Poly (m,(p + q))) . b = (0. F) + (0. F) by defPg
.= ((Poly (m,p)) . b) + (0. F) by H, defPg
.= ((Poly (m,p)) . b) + ((Poly (m,q)) . b) by H, defPg
.= ((Poly (m,p)) + (Poly (m,q))) . b by POLYNOM1:15 ;
hence (Poly (m,(p + q))) . o = ((Poly (m,p)) + (Poly (m,q))) . o ; :: thesis: verum

end;

end;

end;

hence Poly (m,(p + q)) = (Poly (m,p)) + (Poly (m,q)) by I; :: thesis: verum