let c be complex number ; :: thesis: for g, h being complex-valued Function holds (g (#) h) (/) c = g (#) (h (/) c)
let g, h be complex-valued Function; :: thesis: (g (#) h) (/) c = g (#) (h (/) c)
A1: dom ((g (#) h) (/) c) = dom (g (#) h) by VALUED_1:def 5;
( dom (g (#) h) = (dom g) /\ (dom h) & dom (h (/) c) = dom h ) by VALUED_1:def 4, VALUED_1:def 5;
hence dom ((g (#) h) (/) c) = dom (g (#) (h (/) c)) by A1, VALUED_1:def 4; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((g (#) h) (/) c) or ((g (#) h) (/) c) . b₁ = (g (#) (h (/) c)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((g (#) h) (/) c) or ((g (#) h) (/) c) . x = (g (#) (h (/) c)) . x )
assume x in dom ((g (#) h) (/) c) ; :: thesis: ((g (#) h) (/) c) . x = (g (#) (h (/) c)) . x
thus ((g (#) h) (/) c) . x = ((g (#) h) . x) * (c ") by VALUED_1:6
.= ((g . x) * (h . x)) * (c ") by VALUED_1:5
.= (g . x) * ((h . x) * (c "))
.= (g . x) * ((h (/) c) . x) by VALUED_1:6
.= (g (#) (h (/) c)) . x by VALUED_1:5 ; :: thesis: verum