let c be complex number ; :: thesis: for f, g being complex-valued Function holds (f (/) c) + (g (/) c) = (f + g) (/) c
let f, g be complex-valued Function; :: thesis: (f (/) c) + (g (/) c) = (f + g) (/) c
A1: dom ((f (/) c) + (g (/) c)) = (dom (f (/) c)) /\ (dom (g (/) c)) by VALUED_1:def 1;
A2: dom (f (/) c) = dom f by VALUED_2:28;
A3: dom (g (/) c) = dom g by VALUED_2:28;
A4: dom ((f + g) (/) c) = dom (f + g) by VALUED_2:28;
A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
thus dom ((f (/) c) + (g (/) c)) = dom ((f + g) (/) c) by A1, A2, A3, A4, VALUED_1:def 1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((f (/) c) + (g (/) c)) or ((f (/) c) + (g (/) c)) . b₁ = ((f + g) (/) c) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((f (/) c) + (g (/) c)) or ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x )
assume A6: x in dom ((f (/) c) + (g (/) c)) ; :: thesis: ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x
thus ((f + g) (/) c) . x = ((f + g) . x) / c by VALUED_2:29
.= ((f . x) + (g . x)) / c by A1, A2, A3, A6, A5, VALUED_1:def 1
.= ((f . x) / c) + ((g . x) / c)
.= ((f . x) / c) + ((g (/) c) . x) by VALUED_2:29
.= ((f (/) c) . x) + ((g (/) c) . x) by VALUED_2:29
.= ((f (/) c) + (g (/) c)) . x by A6, VALUED_1:def 1 ; :: thesis: verum