let E be RealNormSpace; :: thesis: for a being Point of E
for f being Real_Sequence holds f (#) (NAT --> a) = f * a
let a be Point of E; :: thesis: for f being Real_Sequence holds f (#) (NAT --> a) = f * a
let f be Real_Sequence; :: thesis: f (#) (NAT --> a) = f * a
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (f (#) (NAT --> a)) . n = (f * a) . n
thus (f (#) (NAT --> a)) . n = (f . n) * ((NAT --> a) . n) by NDIFF_1:def 2
.= (f * a) . n by NDIFF_1:def 3 ; :: thesis: verum