reconsider f = NAT --> (0. R) as sequence of the carrier of R ;
take f ; :: thesis: f is finite-Support
take 0 ; :: according to ALGSEQ_1:def 1 :: thesis: for i being Nat st i >= 0 holds
f . i = 0. R
let i be Nat; :: thesis: ( i >= 0 implies f . i = 0. R )
thus ( i >= 0 implies f . i = 0. R ) by FUNCOP_1:7, ORDINAL1:def 12; :: thesis: verum