let i, j be Nat; :: thesis: for xi being Element of (REAL-NS 1) st 1 <= i & i <= j holds
||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.||
let xi be Element of (REAL-NS 1); :: thesis: ( 1 <= i & i <= j implies ||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.|| )
assume A1: ( 1 <= i & i <= j ) ; :: thesis: ||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.||
consider q being Element of REAL , y being Element of REAL j such that
A2: ( xi = <*q*> & y = 0. (REAL-NS j) & (reproj (i,(0. (REAL-NS j)))) . xi = (reproj (i,y)) . q ) by PDIFF_1:def 6;
A3: (reproj (i,(0. (REAL-NS j)))) . xi = Replace (y,i,q) by A2, PDIFF_1:def 5;
len y = j by CARD_1:def 7;
then (reproj (i,(0. (REAL-NS j)))) . xi = ((y | (i -' 1)) ^ <*q*>) ^ (y /^ i) by A1, A3, FINSEQ_7:def 1;
then A4: ||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = |.(((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)).| by A2, REAL_NS1:1;
y | (i -' 1) = (0* j) | (i -' 1) by A2, REAL_NS1:def 4;
then sqrt (Sum (sqr (y | (i -' 1)))) = |.(0* (i -' 1)).| by A1, Th2;
then sqrt (Sum (sqr (y | (i -' 1)))) = 0 by EUCLID:7;
then A5: Sum (sqr (y | (i -' 1))) = 0 by RVSUM_1:86, SQUARE_1:24;
y /^ i = (0* j) /^ i by A2, REAL_NS1:def 4;
then sqrt (Sum (sqr (y /^ i))) = |.(0* (j -' i)).| by Th3;
then A6: sqrt (Sum (sqr (y /^ i))) = 0 by EUCLID:7;
reconsider q2 = q ^2 as Real ;
sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)) = (sqr ((y | (i -' 1)) ^ <*q*>)) ^ (sqr (y /^ i)) by RVSUM_1:144
.= ((sqr (y | (i -' 1))) ^ (sqr <*q*>)) ^ (sqr (y /^ i)) by RVSUM_1:144
.= ((sqr (y | (i -' 1))) ^ <*(q ^2)*>) ^ (sqr (y /^ i)) by RVSUM_1:55 ;
then Sum (sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i))) = (Sum ((sqr (y | (i -' 1))) ^ <*q2*>)) + (Sum (sqr (y /^ i))) by RVSUM_1:75
.= ((Sum (sqr (y | (i -' 1)))) + (q ^2)) + (Sum (sqr (y /^ i))) by RVSUM_1:74
.= q ^2 by A5, A6, RVSUM_1:86, SQUARE_1:24 ;
then A7: ||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = |.q.| by A4, COMPLEX1:72;
(proj (1,1)) . <*q*> = q by PDIFF_1:1;
hence ||.((reproj (i,(0. (REAL-NS j)))) . xi).|| = ||.xi.|| by A7, A2, PDIFF_1:4; :: thesis: verum