let F1, F2 be Field; :: thesis: ( F1 is Subfield of F2 & F2 is Subfield of F1 implies for f being Function of F1,F2 st f = id F1 holds
f is isomorphism )
assume AS1: ( F1 is Subfield of F2 & F2 is Subfield of F1 ) ; :: thesis: for f being Function of F1,F2 st f = id F1 holds
f is isomorphism
let f be Function of F1,F2; :: thesis: ( f = id F1 implies f is isomorphism )
assume AS2: f = id F1 ; :: thesis: f is isomorphism
( the carrier of F1 c= the carrier of F2 & the carrier of F2 c= the carrier of F1 ) by AS1, EC_PF_1:def 1;
then A: the carrier of F2 = the carrier of F1 by TARSKI:2;
C: the addF of F1 = the addF of F2 || the carrier of F1 by AS1, EC_PF_1:def 1
.= the addF of F2 by A ;
D: the multF of F1 = the multF of F2 || the carrier of F1 by AS1, EC_PF_1:def 1
.= the multF of F2 by A ;
( f is additive & f is multiplicative & f is unity-preserving ) by C, D, AS2, AS1, EC_PF_1:def 1;
hence f is isomorphism by A, AS2; :: thesis: verum