:: deftheorem Def1 defines finite-Support ALGSEQ_1:def 1 :
for R being non empty ZeroStr
for F being sequence of R holds
( F is finite-Support iff ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R );