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

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