let c be Complex; for f, g being complex-valued Function holds (f (/) c) + (g (/) c) = (f + g) (/) c
let f, g be complex-valued Function; (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; FUNCT_1:def 11 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 ; ( 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))
; ((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
; verum