let g, h, k be complex-valued Function; :: thesis: (g /" h) (#) k = (g (#) k) /" h
A1: ( dom ((g /" h) (#) k) = (dom (g /" h)) /\ (dom k) & dom ((g (#) k) /" h) = (dom (g (#) k)) /\ (dom h) ) by VALUED_1:16, VALUED_1:def 4;
( dom (g /" h) = (dom g) /\ (dom h) & dom (g (#) k) = (dom g) /\ (dom k) ) by VALUED_1:16, VALUED_1:def 4;
hence dom ((g /" h) (#) k) = dom ((g (#) k) /" h) 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 (#) k) /" h) . b₁ )
let x be object ; :: thesis: ( not x in dom ((g /" h) (#) k) or ((g /" h) (#) k) . x = ((g (#) k) /" h) . x )
assume x in dom ((g /" h) (#) k) ; :: thesis: ((g /" h) (#) k) . x = ((g (#) k) /" h) . x
thus ((g /" h) (#) k) . x = ((g /" h) . x) * (k . x) by VALUED_1:5
.= ((g . x) / (h . x)) * (k . x) by VALUED_1:17
.= ((g . x) * (k . x)) / (h . x)
.= ((g (#) k) . x) / (h . x) by VALUED_1:5
.= ((g (#) k) /" h) . x by VALUED_1:17 ; :: thesis: verum