let f be complex-valued Function; :: thesis: for r, p being Complex holds (r * p) (#) f = r (#) (p (#) f)
let r, p be Complex; :: thesis: (r * p) (#) f = r (#) (p (#) f)
A1: dom ((r * p) (#) f) = dom f by VALUED_1:def 5
.= dom (p (#) f) by VALUED_1:def 5
.= dom (r (#) (p (#) f)) by VALUED_1:def 5 ;

now :: thesis: for c being object st c in dom ((r * p) (#) f) holds
((r * p) (#) f) . c = (r (#) (p (#) f)) . c

let c be object ; :: thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) . c = (r (#) (p (#) f)) . c )
assume A2: c in dom ((r * p) (#) f) ; :: thesis: ((r * p) (#) f) . c = (r (#) (p (#) f)) . c
then A3: c in dom (p (#) f) by A1, VALUED_1:def 5;
thus ((r * p) (#) f) . c = (r * p) * (f . c) by A2, VALUED_1:def 5
.= r * (p * (f . c))
.= r * ((p (#) f) . c) by A3, VALUED_1:def 5
.= (r (#) (p (#) f)) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

hence (r * p) (#) f = r (#) (p (#) f) by A1, FUNCT_1:2; :: thesis: verum