let i, j be Element of NAT ; for x being Element of REAL j holds x = (reproj (i,x)) . ((proj (i,j)) . x)
let x be Element of REAL j; x = (reproj (i,x)) . ((proj (i,j)) . x)
set q = (reproj (i,x)) . ((proj (i,j)) . x);
A1:
( dom ((reproj (i,x)) . ((proj (i,j)) . x)) = Seg j & dom x = Seg j )
by FINSEQ_1:89;
A2:
len x = j
by A1, FINSEQ_1:def 3;
for k being Nat st k in dom x holds
x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k
proof
let k be
Nat;
( k in dom x implies x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k )
assume A3:
k in dom x
;
x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k
then A4:
( 1
<= k &
k <= j )
by A1, FINSEQ_1:1;
(reproj (i,x)) . ((proj (i,j)) . x) = Replace (
x,
i,
((proj (i,j)) . x))
by PDIFF_1:def 5;
then A5:
((reproj (i,x)) . ((proj (i,j)) . x)) . k = (Replace (x,i,((proj (i,j)) . x))) /. k
by A3, A1, PARTFUN1:def 6;
end;
hence
x = (reproj (i,x)) . ((proj (i,j)) . x)
by A1, FINSEQ_1:13; verum