let K be Field; :: thesis: for SK1, SK2 being Subfield of K holds
( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 )
let SK1, SK2 be Subfield of K; :: thesis: ( SK1 is Subfield of SK2 iff the carrier of SK1 c= the carrier of SK2 )
set C1 = the carrier of SK1;
set C2 = the carrier of SK2;
set ADD = the addF of K;
set MULT = the multF of K;
thus ( SK1 is Subfield of SK2 implies the carrier of SK1 c= the carrier of SK2 ) by Def1; :: thesis: ( the carrier of SK1 c= the carrier of SK2 implies SK1 is Subfield of SK2 )
assume A1: the carrier of SK1 c= the carrier of SK2 ; :: thesis: SK1 is Subfield of SK2
then A2: [: the carrier of SK1, the carrier of SK1:] c= [: the carrier of SK2, the carrier of SK2:] by ZFMISC_1:96;
the addF of SK2 = the addF of K || the carrier of SK2 by Def1;
then A3: the addF of SK2 || the carrier of SK1 = the addF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the addF of SK1 by Def1 ;
the multF of SK2 = the multF of K || the carrier of SK2 by Def1;
then A4: the multF of SK2 || the carrier of SK1 = the multF of K || the carrier of SK1 by A2, FUNCT_1:51
.= the multF of SK1 by Def1 ;
( 1. SK1 = 1. K & 0. SK1 = 0. K ) by Def1;
then ( 1. SK1 = 1. SK2 & 0. SK1 = 0. SK2 ) by Def1;
hence SK1 is Subfield of SK2 by A1, A3, A4, Def1; :: thesis: verum