let j be Element of NAT ; :: thesis: for q being Real
for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
let q be Real; :: thesis: for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
let i be Nat; :: thesis: ( 1 <= i & i <= j implies |.((reproj (i,(0* j))) . q).| = |.q.| )
assume A1: ( 1 <= i & i <= j ) ; :: thesis: |.((reproj (i,(0* j))) . q).| = |.q.|
reconsider q = q as Element of REAL by XREAL_0:def 1;
set y = 0* j;
A2: (reproj (i,(0* j))) . q = Replace ((0* j),i,q) by PDIFF_1:def 5;
0* j in j -tuples_on REAL ;
then ex s being Element of REAL * st
( s = 0* j & len s = j ) ;
then A3: (reproj (i,(0* j))) . q = (((0* j) | (i -' 1)) ^ <*q*>) ^ ((0* j) /^ i) by A1, A2, FINSEQ_7:def 1;
sqrt (Sum (sqr ((0* j) | (i -' 1)))) = |.(0* (i -' 1)).| by A1, PDIFF_7:2;
then sqrt (Sum (sqr ((0* j) | (i -' 1)))) = 0 by EUCLID:7;
then A4: Sum (sqr ((0* j) | (i -' 1))) = 0 by RVSUM_1:86, SQUARE_1:24;
sqrt (Sum (sqr ((0* j) /^ i))) = |.(0* (j -' i)).| by PDIFF_7:3;
then A5: sqrt (Sum (sqr ((0* j) /^ i))) = 0 by EUCLID:7;
reconsider q2 = q ^2 as Element of REAL by XREAL_0:def 1;
sqr ((((0* j) | (i -' 1)) ^ <*q*>) ^ ((0* j) /^ i)) = (sqr (((0* j) | (i -' 1)) ^ <*q*>)) ^ (sqr ((0* j) /^ i)) by TOPREAL7:10
.= ((sqr ((0* j) | (i -' 1))) ^ (sqr <*q*>)) ^ (sqr ((0* j) /^ i)) by TOPREAL7:10
.= ((sqr ((0* j) | (i -' 1))) ^ <*(q ^2)*>) ^ (sqr ((0* j) /^ i)) by RVSUM_1:55 ;
then Sum (sqr ((((0* j) | (i -' 1)) ^ <*q*>) ^ ((0* j) /^ i))) = (Sum ((sqr ((0* j) | (i -' 1))) ^ <*q2*>)) + (Sum (sqr ((0* j) /^ i))) by RVSUM_1:75
.= ((Sum (sqr ((0* j) | (i -' 1)))) + (q ^2)) + (Sum (sqr ((0* j) /^ i))) by RVSUM_1:74
.= q ^2 by A4, A5, RVSUM_1:86, SQUARE_1:24 ;
hence |.((reproj (i,(0* j))) . q).| = |.q.| by A3, COMPLEX1:72; :: thesis: verum