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:18
.= x * y by AS ; :: thesis: verum