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 that
A1: x = a and
A2: y = b ; :: thesis: x - y = a - b
- y = - b by A2, Th4;
hence x - y = a - b by A1, Th2; :: thesis: verum