let r, q be Complex; :: thesis: for f being complex-valued Function holds (r * q) (#) f = r (#) (q (#) f)
let f be complex-valued Function; :: thesis: (r * q) (#) f = r (#) (q (#) f)
thus A1: dom ((r * q) (#) f) = dom f by VALUED_1:def 5
.= dom (q (#) f) by VALUED_1:def 5
.= dom (r (#) (q (#) f)) by VALUED_1:def 5 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((r * q) (#) f) or ((r * q) (#) f) . b₁ = (r (#) (q (#) f)) . b₁ )
let c be object ; :: thesis: ( not c in dom ((r * q) (#) f) or ((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, VALUED_1:def 5;
thus ((r * q) (#) f) . c = (r * q) * (f . c) by A2, VALUED_1:def 5
.= r * (q * (f . c))
.= r * ((q (#) f) . c) by A3, VALUED_1:def 5
.= (r (#) (q (#) f)) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum