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 p9 = p, q9 = q as Element of REAL 1 by EUCLID:22;
x + y = p9 + q9 by A1, A2, A3, Th14;
hence x + y = p + q ; :: thesis: verum