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

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