set f = NAT --> (0. R);
reconsider f = NAT --> (0. R) as Function of NAT ,the carrier of R ;
take f ; :: thesis: f is finite-Support
take 0 ; :: according to ALGSEQ_1:def 2 :: 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 )
assume i >= 0 ; :: thesis: f . i = 0. R
i in NAT by ORDINAL1:def 13;
hence f . i = 0. R by FUNCOP_1:13; :: thesis: verum