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

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