let T be RealLinearSpace; :: thesis: for x, y being Element of T
for p, q being Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x & q = y holds
x - y = p - q
let x, y be Element of T; :: thesis: for p, q being Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x & q = y holds
x - y = p - q
let p, q be Element of (TOP-REAL 1); :: thesis: ( T = TOP-REAL 1 & p = x & q = y implies x - y = p - q )
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y ; :: thesis: x - y = p - q
reconsider y9 = - y as Element of T ;
reconsider q = q as Element of REAL 1 by EUCLID:22;
reconsider q9 = - q as Element of (TOP-REAL 1) by EUCLID:22;
- q = - y by A1, A3, Th17;
hence x - y = p - q by A1, A2, Th19; :: thesis: verum