let g be Function of A,F_Complex; :: thesis: ( g = f *' implies g is additive )

assume A1: g = f *' ; :: thesis: g is additive

A2: dom g = the carrier of A by FUNCT_2:def 1;

let x, y be Element of A; :: according to VECTSP_1:def 19 :: thesis: 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 ;

:: thesis: verum

assume A1: g = f *' ; :: thesis: g is additive

A2: dom g = the carrier of A by FUNCT_2:def 1;

let x, y be Element of A; :: according to VECTSP_1:def 19 :: thesis: 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 ;

:: thesis: verum