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

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