let j be Element of NAT ; for q being Real
for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
let q be Real; for i being Nat st 1 <= i & i <= j holds
|.((reproj (i,(0* j))) . q).| = |.q.|
let i be Nat; ( 1 <= i & i <= j implies |.((reproj (i,(0* j))) . q).| = |.q.| )
assume A1:
( 1 <= i & i <= j )
; |.((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; verum