let E be RealNormSpace; :: thesis: for a being Point of E

for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a

let a be Point of E; :: thesis: for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a

let f be convergent Real_Sequence; :: thesis: lim (f * a) = (lim f) * a

f (#) (NAT --> a) = f * a by Th8;

hence lim (f * a) = (lim f) * (lim (NAT --> a)) by NDIFF_1:14, NDIFF_1:18

.= (lim f) * a by Th9 ;

:: thesis: verum

for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a

let a be Point of E; :: thesis: for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a

let f be convergent Real_Sequence; :: thesis: lim (f * a) = (lim f) * a

f (#) (NAT --> a) = f * a by Th8;

hence lim (f * a) = (lim f) * (lim (NAT --> a)) by NDIFF_1:14, NDIFF_1:18

.= (lim f) * a by Th9 ;

:: thesis: verum