let C be non empty set ; :: thesis: for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let c be Element of C; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let f be PartFunc of C,V; :: thesis: for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)
let r be Real; :: thesis: ( f is total implies (r (#) f) /. c = r * (f /. c) )
assume f is total ; :: thesis: (r (#) f) /. c = r * (f /. c)
then dom (r (#) f) = C by PARTFUN1:def 2;
hence (r (#) f) /. c = r * (f /. c) by Def4; :: thesis: verum