let r be Real; :: thesis: lim (NAT --> r) = r
thus lim (NAT --> r) = (NAT --> r) . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ; :: thesis: verum