let R be non degenerated comRing; :: thesis: for f being sequence of R st Support f is finite holds
f is finite-Support sequence of R
let f be sequence of R; :: thesis: ( Support f is finite implies f is finite-Support sequence of R )
A1: dom f = NAT by FUNCT_2:def 1;
assume A2: Support f is finite ; :: thesis: f is finite-Support sequence of R

per cases ( Support f = {} or Support f <> {} ) ;

suppose Support f = {} ; :: thesis: f is finite-Support sequence of R

then f = 0_. R by Th1;
hence f is finite-Support sequence of R ; :: thesis: verum

end;

suppose Support f <> {} ; :: thesis: f is finite-Support sequence of R

then reconsider S = Support f as non empty finite Subset of NAT by A2;
reconsider m = max S as Element of NAT by ORDINAL1:def 12;
A3: for s being Element of S holds m >= s by XXREAL_2:4;
for i being Nat st i >= m + 1 holds
f . i = 0. R

proof

let i be Nat; :: thesis: ( i >= m + 1 implies f . i = 0. R )
assume A4: i >= m + 1 ; :: thesis: f . i = 0. R
assume A5: f . i <> 0. R ; :: thesis: contradiction
i in dom f by A1, ORDINAL1:def 12;
then i in Support f by A5, POLYNOM1:def 4;
hence contradiction by A4, A3, NAT_1:13; :: thesis: verum

end;

hence f is finite-Support sequence of R by ALGSEQ_1:def 1; :: thesis: verum

end;

end;