let n be Nat; :: thesis: for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
- q = - g
let q be Element of (TOP-REAL n); :: thesis: for g being Element of (REAL-NS n) st q = g holds
- q = - g
let g be Element of (REAL-NS n); :: thesis: ( q = g implies - q = - g )
assume A1: q = g ; :: thesis: - q = - g
thus - q = (- 1) * q by RLVECT_1:16
.= (- 1) * g by A1, Th8
.= - g by RLVECT_1:16 ; :: thesis: verum