let x, y, z, w be Real; :: thesis: for vx, vy being Point of (REAL-NS 2) st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )
let vx, vy be Point of (REAL-NS 2); :: thesis: ( vx = <*x,y*> & vy = <*z,w*> implies ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) )
assume A1: ( vx = <*x,y*> & vy = <*z,w*> ) ; :: thesis: ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )
reconsider vx1 = vx, vy1 = vy as Element of REAL 2 by REAL_NS1:def 4;
thus vx + vy = vx1 + vy1 by REAL_NS1:2
.= <*(x + z),(y + w)*> by A1, Lm7 ; :: thesis: vx - vy = <*(x - z),(y - w)*>
thus vx - vy = vx1 - vy1 by REAL_NS1:5
.= <*(x - z),(y - w)*> by A1, Lm7 ; :: thesis: verum