let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
let f be PartFunc of C,COMPLEX; :: thesis: for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
let r, q be Element of COMPLEX ; :: thesis: (r * q) (#) f = r (#) (q (#) f)
A1: dom ((r * q) (#) f) = dom f by Th7
.= dom (q (#) f) by Th7
.= dom (r (#) (q (#) f)) by Th7 ;

now

let c be Element of C; :: thesis: ( c in dom ((r * q) (#) f) implies ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c )
assume A2: c in dom ((r * q) (#) f) ; :: thesis: ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c
then A3: c in dom (q (#) f) by A1, Th7;
thus ((r * q) (#) f) /. c = (r * q) * (f /. c) by A2, Th7
.= r * (q * (f /. c))
.= r * ((q (#) f) /. c) by A3, Th7
.= (r (#) (q (#) f)) /. c by A1, A2, Th7 ; :: thesis: verum

end;

hence (r * q) (#) f = r (#) (q (#) f) by A1, PARTFUN2:1; :: thesis: verum