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

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:16;
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 GROUP_6:def 6
.= (g . a1) * (g . a2) by H, A2, FIELD_6:16 ; :: thesis: verum

end;

hence g is multiplicative ; :: thesis: verum