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 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 )
assume i >= 0 ; :: thesis: f . i = 0. R
i in NAT by ORDINAL1:def 12;
hence f . i = 0. R by FUNCOP_1:7; :: thesis: verum