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

let x be object ; :: thesis: ( not x in dom ((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
.= ((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 ; :: thesis: verum