let n be Nat; :: thesis: for a being Real
for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
let a be Real; :: thesis: for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
let x1, y1 be Point of (REAL-NS n); :: thesis: for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
reconsider x = x1, y = y1 as Element of REAL n by Def4;
let x2, y2 be Point of (REAL-US n); :: thesis: ( x1 = x2 & y1 = y2 implies ( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 ) )
assume that
A1: x1 = x2 and
A2: y1 = y2 ; :: thesis: ( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )
thus x1 + y1 = (Euclid_add n) . (x,y) by Def4
.= x2 + y2 by A1, A2, Def6 ; :: thesis: ( - x1 = - x2 & a * x1 = a * x2 )
thus - x1 = (- 1) * x1 by RLVECT_1:16
.= (Euclid_mult n) . ((- 1),x) by Def4
.= (- 1) * x2 by A1, Def6
.= - x2 by RLVECT_1:16 ; :: thesis: a * x1 = a * x2
thus a * x1 = (Euclid_mult n) . (a,x) by Def4
.= a * x2 by A1, Def6 ; :: thesis: verum