let i, j be Element of 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 FINSEQ_1:def 18;
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:10;
then A5: Sum (sqr (y | (i -' 1))) = 0 by SQUARE_1:92, RVSUM_1:116;
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:10;
sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)) = (sqr ((y | (i -' 1)) ^ <*q*>)) ^ (sqr (y /^ i)) by TOPREAL7:11
.= ((sqr (y | (i -' 1))) ^ (sqr <*q*>)) ^ (sqr (y /^ i)) by TOPREAL7:11
.= ((sqr (y | (i -' 1))) ^ <*(q ^2 )*>) ^ (sqr (y /^ i)) by RVSUM_1:81 ;
then Sum (sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i))) = (Sum ((sqr (y | (i -' 1))) ^ <*(q ^2 )*>)) + (Sum (sqr (y /^ i))) by RVSUM_1:105
.= ((Sum (sqr (y | (i -' 1)))) + (q ^2 )) + (Sum (sqr (y /^ i))) by RVSUM_1:104
.= q ^2 by A5, A6, SQUARE_1:92, RVSUM_1:116 ;
then A7: ||.((reproj i,(0. (REAL-NS j))) . xi).|| = |.q.| by A4, COMPLEX1:158;
(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