let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds
( p = 0_ (n,R) iff Support p = {} )
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds
( p = 0_ (n,R) iff Support p = {} )
let p be Polynomial of n,R; :: thesis: ( p = 0_ (n,R) iff Support p = {} )

A: now :: thesis: ( p = 0_ (n,R) implies Support p = {} )

assume B: p = 0_ (n,R) ; :: thesis: Support p = {}

now :: thesis: for o being object holds not o in Support p

let o be object ; :: thesis: not o in Support p
assume C: o in Support p ; :: thesis: contradiction
then reconsider b1 = o as Element of Bags n ;
p . b1 <> 0. R by C, POLYNOM1:def 4;
hence contradiction by B, POLYNOM1:22; :: thesis: verum

end;

hence Support p = {} by XBOOLE_0:def 1; :: thesis: verum

end;

now :: thesis: ( Support p = {} implies p = 0_ (n,R) )

assume Support p = {} ; :: thesis: p = 0_ (n,R)
then p = (Bags n) --> (0. R) by POLYNOM1:def 4;
hence p = 0_ (n,R) by POLYNOM1:def 8; :: thesis: verum

end;

hence ( p = 0_ (n,R) iff Support p = {} ) by A; :: thesis: verum