set n = card (nonConstantPolys F);
let r1, r2 be Polynomial of (card (nonConstantPolys F)),F; :: thesis: ( r1 . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
r1 . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
r1 . b = 0. F ) & r2 . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
r2 . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
r2 . b = 0. F ) implies r1 = r2 )
assume that
A3: ( r1 . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
r1 . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
r1 . b = 0. F ) ) and
A4: ( r2 . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
r2 . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
r2 . b = 0. F ) ) ; :: thesis: r1 = r2
A5: dom r1 = Bags (card (nonConstantPolys F)) by FUNCT_2:def 1
.= dom r2 by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom r1 holds
r1 . o = r2 . o

let o be object ; :: thesis: ( o in dom r1 implies r1 . b₁ = r2 . b₁ )
assume o in dom r1 ; :: thesis: r1 . b₁ = r2 . 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: r1 . b₁ = r2 . b₁

then for i being object st i in card (nonConstantPolys F) holds
b . i = {} by PRE_POLY:def 7;
then b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6;
hence r1 . o = r2 . o by A4, A3; :: thesis: verum

end;

suppose H: support b = {m} ; :: thesis: r1 . b₁ = r2 . b₁

then r1 . b = p . (b . m) by A3
.= r2 . b by H, A4 ;
hence r1 . o = r2 . o ; :: thesis: verum

end;

suppose H: ( support b <> {} & support b <> {m} ) ; :: thesis: r1 . b₁ = r2 . b₁

then r1 . b = 0. F by A3
.= r2 . b by H, A4 ;
hence r1 . o = r2 . o ; :: thesis: verum

end;

end;

end;

hence r1 = r2 by A5; :: thesis: verum