let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

let x be Element of X; :: thesis: ( x in dom (lim f) implies (lim f) . x = lim (R_EAL (f # x)) )

assume x in dom (lim f) ; :: thesis: (lim f) . x = lim (R_EAL (f # x))

then (lim f) . x = lim ((R_EAL f) # x) by MESFUNC8:def 9;

hence (lim f) . x = lim (R_EAL (f # x)) by Th1; :: thesis: verum

for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

let x be Element of X; :: thesis: ( x in dom (lim f) implies (lim f) . x = lim (R_EAL (f # x)) )

assume x in dom (lim f) ; :: thesis: (lim f) . x = lim (R_EAL (f # x))

then (lim f) . x = lim ((R_EAL f) # x) by MESFUNC8:def 9;

hence (lim f) . x = lim (R_EAL (f # x)) by Th1; :: thesis: verum