let R be non degenerated comRing; :: thesis: for f being sequence of R st f is finite-Support sequence of R holds
Support f is finite
let f be sequence of R; :: thesis: ( f is finite-Support sequence of R implies Support f is finite )
assume A1: f is finite-Support sequence of R ; :: thesis: Support f is finite
consider n1 being Nat such that
A2: for i being Nat st i >= n1 holds
f . i = 0. R by A1, ALGSEQ_1:def 1;
A3: for m being Element of NAT st m in Support f holds
m < n1

proof

let m be Element of NAT ; :: thesis: ( m in Support f implies m < n1 )
assume m in Support f ; :: thesis: m < n1
then A4: f . m <> 0. R by POLYNOM1:def 4;
assume n1 <= m ; :: thesis: contradiction
hence contradiction by A4, A2; :: thesis: verum

end;

Support f c= Segm n1 by A3, NAT_1:44;
hence Support f is finite ; :: thesis: verum