let T be RealLinearSpace; :: thesis: for x, y being Element of T
for p, q being Tuple of 1, REAL 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 Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y holds
x - y = p - q
let p, q be Tuple of 1, REAL ; :: 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
set p9 = p;
set q9 = q;
reconsider y9 = - y as Element of T ;
reconsider qm9 = - q as Tuple of 1, REAL by Th15;
A4: ( p in Funcs ((Seg 1),REAL) & qm9 is Element of Funcs ((Seg 1),REAL) ) by SRINGS_5:11;
A5: the addF of RLSStruct(# the carrier of (TOP-REAL 1), the ZeroF of (TOP-REAL 1), the addF of (TOP-REAL 1), the Mult of (TOP-REAL 1) #) . (p,qm9) = the addF of (RealVectSpace (Seg 1)) . (p,qm9) by EUCLID:def 8
.= p + qm9 by A4, FUNCSDOM:def 1 ;
x - y = the addF of (TOP-REAL 1) . (x,(- y)) by A1, ALGSTR_0:def 1
.= p - q by A5, A1, A2, A3, Th16 ;
hence x - y = p - q ; :: thesis: verum