let r be Element of REAL ; :: thesis: lim (NAT --> r) = r
thus lim (NAT --> r) = (NAT --> r) . 0 by SEQ_4:26
.= r ; :: thesis: verum