let c1, c2 be complex number ; :: 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)
A2: dom (g (/) c1) = dom g by VALUED_1:def 5;
dom (g (/) (c1 * c2)) = dom g by VALUED_1:def 5;
hence dom ((g (/) c1) (/) c2) = dom (g (/) (c1 * c2)) by A2, VALUED_1:def 5; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom ((g (/) c1) (/) c2) or ((g (/) c1) (/) c2) . b₁ = (g (/) (c1 * c2)) . b₁ )
let x be set ; :: 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:205
.= (g (/) (c1 * c2)) . x by VALUED_1:6 ; :: thesis: verum