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
A1: (NAT --> a) . n = a by FUNCOP_1:7;
thus (f (#) (NAT --> a)) . n = (f . n) * ((NAT --> a) . n) by NDIFF_1:def 2
.= (f * a) . n by A1, NDIFF_1:def 3 ; :: thesis: verum