let T be RealLinearSpace; :: thesis: for x being Element of T
for p being Tuple of 1, REAL st T = TOP-REAL 1 & p = x holds
- p = - x
let x be Element of T; :: thesis: for p being Tuple of 1, REAL st T = TOP-REAL 1 & p = x holds
- p = - x
let p be Tuple of 1, REAL ; :: thesis: ( T = TOP-REAL 1 & p = x implies - p = - x )
assume that
A1: T = TOP-REAL 1 and
A2: p = x ; :: thesis: - p = - x
consider d being Element of REAL such that
A3: p = <*d*> by FINSEQ_2:97;
reconsider x9 = <*(- d)*> as Tuple of 1, REAL ;
reconsider n = 1 as Nat ;
( not REAL is empty & REAL c= REAL ) ;
then reconsider p9 = p as Element of 1 -tuples_on REAL by FINSEQ_2:109;
A4: ( 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) #) = RealVectSpace (Seg 1) & 0.REAL 1 = <*0*> ) by EUCLID:def 8, FINSEQ_2:59;
A5: p + (- p) = p9 + (- p9)
.= 0. (TOP-REAL 1) by A4, RVSUM_1:22 ;
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def 8;
then reconsider x99 = x9 as Element of T by A1;
A6: - p = <*(- d)*> by A3, RVSUM_1:20;
x + x99 = 0. T by A1, A2, A6, Th14, A5;
then - x = x99 by RLVECT_1:def 10;
hence - p = - x by A3, RVSUM_1:20; :: thesis: verum