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
Proj (- p),i = - (Proj p,i)
let p be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
Proj (- p),i = - (Proj p,i)
let i be Element of NAT ; :: thesis: ( i in Seg n implies Proj (- p),i = - (Proj p,i) )
assume A1: i in Seg n ; :: thesis: Proj (- p),i = - (Proj p,i)
reconsider w1 = p as Element of REAL n by EUCLID:25;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w = - p as Element of REAL n by EUCLID:25;
len w1 = n by FINSEQ_1:def 18;
then A2: i in dom w1 by A1, FINSEQ_1:def 3;
A3: Proj p,i = w1 /. i by Def1
.= w3 . i by A2, PARTFUN1:def 8 ;
len w = n by FINSEQ_1:def 18;
then A4: i in dom w by A1, FINSEQ_1:def 3;
Proj (- p),i = w /. i by Def1
.= w . i by A4, PARTFUN1:def 8
.= (- w3) . i by A4, EUCLID:72
.= (- 1) * (Proj p,i) by A3, RVSUM_1:67
.= - (Proj p,i) ;
hence Proj (- p),i = - (Proj p,i) ; :: thesis: verum