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