let X be RealUnitarySpace; :: thesis: for x being Point of X
for x1 being Point of (RUSp2RNSp X) st x = x1 holds
- x = - x1
let x be Point of X; :: thesis: for x1 being Point of (RUSp2RNSp X) st x = x1 holds
- x = - x1
let x1 be Point of (RUSp2RNSp X); :: thesis: ( x = x1 implies - x = - x1 )
assume AS: x = x1 ; :: thesis: - x = - x1
thus - x = (- 1) * x by RLVECT_1:16
.= (- 1) * x1 by AS
.= - x1 by RLVECT_1:16 ; :: thesis: verum