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

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