let n be Element of 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 A1: ( x = a & y = b ) ; :: thesis: x - y = a - b
then A2: - y = - b by Th4;
thus x - y = a - b by A1, A2, Th2; :: thesis: verum