let s be sequence of L; :: thesis: ( s = (0_. L) +* (n,z) implies s is finite-Support )
assume A1: s = (0_. L) +* (n,z) ; :: thesis: s is finite-Support
take n + 1 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not n + 1 <= b₁ or s . b₁ = 0. L )
let i be Nat; :: thesis: ( not n + 1 <= i or s . i = 0. L )
assume n + 1 <= i ; :: thesis: s . i = 0. L
then n < i by NAT_1:13;
hence s . i = (0_. L) . i by A1, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum