let R be non degenerated comRing; :: thesis: for f being sequence of R holds
( Support f = {} iff f = 0_. R )
let f be sequence of R; :: thesis: ( Support f = {} iff f = 0_. R )
( f = 0_. R implies Support f = {} )

proof

assume A1: f = 0_. R ; :: thesis: Support f = {}
Support f = {}

proof

assume Support f <> {} ; :: thesis: contradiction
then consider o being object such that
A2: o in Support f by XBOOLE_0:def 1;
reconsider x1 = o as Element of NAT by A2;
f . x1 <> 0. R by A2, POLYNOM1:def 4;
hence contradiction by A1; :: thesis: verum

end;

hence Support f = {} ; :: thesis: verum

end;

hence ( Support f = {} iff f = 0_. R ) by POLYNOM1:def 4; :: thesis: verum