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