let c be complex number ; :: thesis: for f, g being complex-valued Function st c <> 0 holds
(f (/) c) - g = (f - (c (#) g)) (/) c
let f, g be complex-valued Function; :: thesis: ( c <> 0 implies (f (/) c) - g = (f - (c (#) g)) (/) c )
assume A1: c <> 0 ; :: thesis: (f (/) c) - g = (f - (c (#) g)) (/) c
A2: dom ((f (/) c) - g) = (dom (f (/) c)) /\ (dom g) by VALUED_1:12
.= (dom f) /\ (dom g) by VALUED_2:28 ;
A3: dom (f - (c (#) g)) = (dom f) /\ (dom (c (#) g)) by VALUED_1:12
.= (dom f) /\ (dom g) by VALUED_1:def 5 ;
hence dom ((f (/) c) - g) = dom ((f - (c (#) g)) (/) c) by A2, VALUED_2:28; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((f (/) c) - g) or ((f (/) c) - g) . b₁ = ((f - (c (#) g)) (/) c) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((f (/) c) - g) or ((f (/) c) - g) . x = ((f - (c (#) g)) (/) c) . x )
assume A4: x in dom ((f (/) c) - g) ; :: thesis: ((f (/) c) - g) . x = ((f - (c (#) g)) (/) c) . x
hence ((f (/) c) - g) . x = ((f (/) c) . x) - (g . x) by VALUED_1:13
.= ((f . x) / c) - (g . x) by VALUED_2:29
.= ((f . x) / c) - ((c * (g . x)) / c) by A1, XCMPLX_1:89
.= ((f . x) / c) - (((c (#) g) . x) / c) by VALUED_1:6
.= ((f . x) - ((c (#) g) . x)) / c
.= ((f - (c (#) g)) . x) / c by A2, A3, A4, VALUED_1:13
.= ((f - (c (#) g)) (/) c) . x by VALUED_2:29 ;
:: thesis: verum