let g be Function of A,F_Complex; ( g = f *' implies g is additive )
assume A1:
g = f *'
; g is additive
A2:
dom g = the carrier of A
by FUNCT_2:def 1;
let x, y be Element of A; VECTSP_1:def 19 g . (x + y) = (g . x) + (g . y)
A3:
( g . x = (f . x) *' & g . y = (f . y) *' )
by A1, A2, COMSEQ_2:def 1;
f . (x + y) = (f . x) + (f . y)
by VECTSP_1:def 20;
hence (g . x) + (g . y) =
(f . (x + y)) *'
by A3, COMPLEX1:32
.=
g . (x + y)
by A1, A2, COMSEQ_2:def 1
;
verum