let S, T be RealNormSpace; :: thesis: for h being PartFunc of S,T
for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let h be PartFunc of S,T; :: thesis: for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let seq be sequence of S; :: thesis: for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let r be Real; :: thesis: ( h is total implies (r (#) h) /* seq = r * (h /* seq) )
assume h is total ; :: thesis: (r (#) h) /* seq = r * (h /* seq)
then dom h = the carrier of S by PARTFUN1:def 2;
then rng seq c= dom h ;
hence (r (#) h) /* seq = r * (h /* seq) by NFCONT_1:13; :: thesis: verum