let g be Function of F,F; :: thesis: ( g = f | the carrier of F implies g is additive )
assume A: g = f | the carrier of F ; :: thesis: g is additive

now :: thesis: for a1, a2 being Element of F holds g . (a1 + a2) = (g . a1) + (g . a2)

let a1, a2 be Element of F; :: thesis: g . (a1 + a2) = (g . a1) + (g . a2)
A0: F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider b1 = a1, b2 = a2 as Element of E ;
H: F is Subring of E by A0, FIELD_5:12;
then A1: a1 + a2 = b1 + b2 by FIELD_6:15;
A2: ( f . b1 = g . a1 & f . b2 = g . a2 ) by A, FUNCT_1:49;
thus g . (a1 + a2) = f . (b1 + b2) by A1, A, FUNCT_1:49
.= (f . b1) + (f . b2) by VECTSP_1:def 20
.= (g . a1) + (g . a2) by H, A2, FIELD_6:15 ; :: thesis: verum

end;

hence g is additive ; :: thesis: verum