let n be Nat; :: thesis: for a being Real
for x, y being Element of (REAL-NS n)
for x0, y0 being Element of (RealVectSpace (Seg n)) st x = x0 & y = y0 holds
( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
let a be Real; :: thesis: for x, y being Element of (REAL-NS n)
for x0, y0 being Element of (RealVectSpace (Seg n)) st x = x0 & y = y0 holds
( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
let x, y be Element of (REAL-NS n); :: thesis: for x0, y0 being Element of (RealVectSpace (Seg n)) st x = x0 & y = y0 holds
( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
let x0, y0 be Element of (RealVectSpace (Seg n)); :: thesis: ( x = x0 & y = y0 implies ( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 ) )
assume A1: ( x = x0 & y = y0 ) ; :: thesis: ( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
A2: RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the U5 of (REAL-NS n), the Mult of (REAL-NS n) #) = RealVectSpace (Seg n) by Th15;
set V = REAL-NS n;
set W = RealVectSpace (Seg n);
thus ( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) ) by A2; :: thesis: ( x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
thus x + y = x0 + y0 by A1, A2; :: thesis: ( a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )
thus a * x = a * x0 by A1, A2; :: thesis: ( - x = - x0 & x - y = x0 - y0 )
thus - x = (- 1) * x by RLVECT_1:16
.= (- 1) * x0 by A1, A2
.= - x0 by RLVECT_1:16 ; :: thesis: x - y = x0 - y0
- y = (- 1) * y by RLVECT_1:16
.= (- 1) * y0 by A1, A2
.= - y0 by RLVECT_1:16 ;
hence x - y = x0 - y0 by A1, A2; :: thesis: verum