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