let x, y be Real; :: thesis: <*x,y*> is Point of (REAL-NS 2)
reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;
<*x1,y1*> in REAL 2 by FINSEQ_2:101;
hence <*x,y*> is Point of (REAL-NS 2) by REAL_NS1:def 4; :: thesis: verum