let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r being Complex holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
let f be PartFunc of C,COMPLEX; :: thesis: for r being Complex holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
let r be Complex; :: thesis: ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
thus A1: dom (r (#) f) = dom f by VALUED_1:def 5; :: thesis: for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c)

now :: thesis: for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c)

let c be Element of C; :: thesis: ( c in dom (r (#) f) implies (r (#) f) /. c = r * (f /. c) )
assume A2: c in dom (r (#) f) ; :: thesis: (r (#) f) /. c = r * (f /. c)
hence (r (#) f) /. c = (r (#) f) . c by PARTFUN1:def 6
.= r * (f . c) by VALUED_1:6
.= r * (f /. c) by A1, A2, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ; :: thesis: verum