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

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