let C be non empty set ; :: thesis: for c being Element of C
for r being Real
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
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
let r be Real; :: 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 ;
then dom (r (#) f) = C ;
hence (r (#) f) . c = r * (f . c) by VALUED_1:def 5; :: thesis: verum