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