let c be Complex; :: 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:16, VALUED_1:def 5;

hence dom ((g /" h) (/) c) = dom (g /" (h (#) c)) by A1, VALUED_1:16; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((g /" h) (/) c) or ((g /" h) (/) c) . b_{1} = (g /" (h (#) c)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((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:17

.= (g . x) / ((h . x) * c) by XCMPLX_1:78

.= (g . x) / ((h (#) c) . x) by VALUED_1:6

.= (g /" (h (#) c)) . x by VALUED_1:17 ; :: thesis: verum

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:16, VALUED_1:def 5;

hence dom ((g /" h) (/) c) = dom (g /" (h (#) c)) by A1, VALUED_1:16; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((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:17

.= (g . x) / ((h . x) * c) by XCMPLX_1:78

.= (g . x) / ((h (#) c) . x) by VALUED_1:6

.= (g /" (h (#) c)) . x by VALUED_1:17 ; :: thesis: verum