let F1, F2 be Field; :: thesis: ( F1 == F2 implies ( 0_. F1 = 0_. F2 & 1_. F1 = 1_. F2 ) )
assume F1 == F2 ; :: thesis: ( 0_. F1 = 0_. F2 & 1_. F1 = 1_. F2 )
then F1 is Subfield of F2 by FIELD_7:def 2;
then A: F2 is FieldExtension of F1 by FIELD_4:7;
hence 0_. F1 = 0_. F2 by FIELD_4:12; :: thesis: 1_. F1 = 1_. F2
thus 1_. F1 = 1_. F2 by A, FIELD_4:14; :: thesis: verum