let C be non empty set ; :: thesis: for c being Element of C
for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let c be Element of C; :: thesis: for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let r be real number ; :: thesis: for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let f be PartFunc of C,REAL ; :: thesis: ( f is total implies (r (#) f) . c = r * (f . c) )
assume f is total ; :: thesis: (r (#) f) . c = r * (f . c)
then r (#) f is total by Th67;
then dom (r (#) f) = C by PARTFUN1:def 4;
hence (r (#) f) . c = r * (f . c) by VALUED_1:def 5; :: thesis: verum