a in F_Rat ;
then a in F_Real by EC_PF_1:3, GAUSSINT:14;
then reconsider aa = a as Element of F_Real ;
b in F_Rat ;
then b in F_Real by EC_PF_1:3, GAUSSINT:14;
then reconsider bb = b as Element of F_Real ;
assume AS: ( a = x & b = y ) ; :: thesis: a + b = x + y
thus a + b = aa + bb by GAUSSINT:14, GAUSSINT:17
.= x + y by AS ; :: thesis: verum