let c be Complex; :: 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 ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((f (/) c) - g) or ((f (/) c) - g) . b1 = ((f - (c (#) g)) (/) c) . b1 )

let x be object ; :: thesis: ( not x in dom ((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
.= ((f . x) / c) - (((c (#) g) . x) / c) by VALUED_1:6
.= ((f . x) - ((c (#) g) . x)) / c
.= ((f - (c (#) g)) . x) / c by
.= ((f - (c (#) g)) (/) c) . x by VALUED_2:29 ;
:: thesis: verum