let E be RealNormSpace; :: thesis: for a being Point of E holds lim (NAT --> a) = a
let a be Point of E; :: thesis: lim (NAT --> a) = a
thus lim (NAT --> a) = (NAT --> a) . 0 by NDIFF_1:18
.= a ; :: thesis: verum