let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
let p be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
let i be Element of NAT ; :: thesis: ( i in Seg n implies (- p) /. i = - (p /. i) )
assume A1: i in Seg n ; :: thesis: (- p) /. i = - (p /. i)
reconsider w1 = p as Element of REAL n by EUCLID:22;
len w1 = n by CARD_1:def 7;
then A2: i in dom w1 by A1, FINSEQ_1:def 3;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
A3: p /. i = w3 . i by A2, PARTFUN1:def 6;
reconsider w = - p as Element of REAL n by EUCLID:22;
len w = n by CARD_1:def 7;
then i in dom w by A1, FINSEQ_1:def 3;
then (- p) /. i = w . i by PARTFUN1:def 6
.= (- w3) . i
.= (- 1) * (p /. i) by A3, RVSUM_1:45
.= - (p /. i) ;
hence (- p) /. i = - (p /. i) ; :: thesis: verum