let c1, c2 be Complex; :: thesis: for g being complex-valued Function holds (g (/) c1) (/) c2 = g (/) (c1 * c2)

let g be complex-valued Function; :: thesis: (g (/) c1) (/) c2 = g (/) (c1 * c2)

( dom (g (/) c1) = dom g & dom (g (/) (c1 * c2)) = dom g ) by VALUED_1:def 5;

hence dom ((g (/) c1) (/) c2) = dom (g (/) (c1 * c2)) by VALUED_1:def 5; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((g (/) c1) (/) c2) or ((g (/) c1) (/) c2) . b_{1} = (g (/) (c1 * c2)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((g (/) c1) (/) c2) or ((g (/) c1) (/) c2) . x = (g (/) (c1 * c2)) . x )

assume x in dom ((g (/) c1) (/) c2) ; :: thesis: ((g (/) c1) (/) c2) . x = (g (/) (c1 * c2)) . x

thus ((g (/) c1) (/) c2) . x = ((g (/) c1) . x) * (c2 ") by VALUED_1:6

.= ((g . x) * (c1 ")) * (c2 ") by VALUED_1:6

.= (g . x) * ((c1 ") * (c2 "))

.= (g . x) * ((c1 * c2) ") by XCMPLX_1:204

.= (g (/) (c1 * c2)) . x by VALUED_1:6 ; :: thesis: verum

let g be complex-valued Function; :: thesis: (g (/) c1) (/) c2 = g (/) (c1 * c2)

( dom (g (/) c1) = dom g & dom (g (/) (c1 * c2)) = dom g ) by VALUED_1:def 5;

hence dom ((g (/) c1) (/) c2) = dom (g (/) (c1 * c2)) by VALUED_1:def 5; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((g (/) c1) (/) c2) or ((g (/) c1) (/) c2) . x = (g (/) (c1 * c2)) . x )

assume x in dom ((g (/) c1) (/) c2) ; :: thesis: ((g (/) c1) (/) c2) . x = (g (/) (c1 * c2)) . x

thus ((g (/) c1) (/) c2) . x = ((g (/) c1) . x) * (c2 ") by VALUED_1:6

.= ((g . x) * (c1 ")) * (c2 ") by VALUED_1:6

.= (g . x) * ((c1 ") * (c2 "))

.= (g . x) * ((c1 * c2) ") by XCMPLX_1:204

.= (g (/) (c1 * c2)) . x by VALUED_1:6 ; :: thesis: verum