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