reconsider t = sqrt 2 as Element of F_Real by XREAL_0:def 1;
B: F_Real is Subfield of F_Complex by FIELD_4:7;
then the carrier of F_Real c= the carrier of F_Complex by EC_PF_1:def 1;
then reconsider t = t as Element of F_Complex ;
sqrt 2 <> 0. F_Real by SQUARE_1:24;
then not t is zero by B, EC_PF_1:def 1;
hence sqrt 2 is non zero Element of F_Complex ; :: thesis: verum