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