let n be Nat; :: thesis: for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b
let x, y be VECTOR of (REAL-NS n); :: thesis: for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b
let a, b be Element of REAL n; :: thesis: ( x = a & y = b implies x + y = a + b )
assume ( x = a & y = b ) ; :: thesis: x + y = a + b
hence x + y = (Euclid_add n) . (a,b) by Def4
.= a + b by Def1 ;
:: thesis: verum