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

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