set F = F_Rat ;
H1: 2. F_Rat = ( the addF of F_Real || the carrier of F_Rat) . [(1. F_Rat),(1. F_Rat)] by GAUSSINT:13
.= addreal . (1,1) by GAUSSINT:13, FUNCT_1:49
.= 1 + 1 by BINOP_2:def 9 ;

now :: thesis: not 2. F_Rat is square

assume 2. F_Rat is square ; :: thesis: contradiction
then consider a being Element of F_Rat such that
A1: a ^2 = 2. F_Rat ;
reconsider a = a as Rational ;
a ^2 = (sqrt 2) ^2 by A1, H1, SQUARE_1:def 2;
then ( a = sqrt 2 or - a = sqrt 2 ) by SQUARE_1:40;
hence contradiction by INT_2:28, IRRAT_1:1; :: thesis: verum

end;

hence not 2. F_Rat is square ; :: thesis: verum