let T be RealLinearSpace; :: thesis: for x being Element of T
for p being Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x holds
- p = - x
let x be Element of T; :: thesis: for p being Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x holds
- p = - x
let p be Element of (TOP-REAL 1); :: thesis: ( T = TOP-REAL 1 & p = x implies - p = - x )
assume that
A1: T = TOP-REAL 1 and
A2: p = x ; :: thesis: - p = - x
p is Element of REAL 1 by EUCLID:22;
then reconsider p9 = p as Tuple of 1, REAL ;
- p9 = - x by A1, A2, Th16;
hence - p = - x ; :: thesis: verum