let j, i be Element of NAT ; :: thesis: for x being Element of REAL j holds x = (reproj (i,x)) . ((proj (i,j)) . x)
let x be Element of REAL j; :: thesis: 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;
A3: 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; :: thesis: ( k in dom x implies x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k )
assume A5: k in dom x ; :: thesis: x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k
then A6: ( 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 A9: ((reproj (i,x)) . ((proj (i,j)) . x)) . k = (Replace (x,i,((proj (i,j)) . x))) /. k by A5, A1, PARTFUN1:def 6;

per cases ( k = i or k <> i ) ;

suppose A10: k = i ; :: thesis: x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k

then ((reproj (i,x)) . ((proj (i,j)) . x)) . k = (proj (i,j)) . x by A3, A6, A9, FINSEQ_7:8;
hence x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k by A10, PDIFF_1:def 1; :: thesis: verum

end;

suppose k <> i ; :: thesis: x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k

then ((reproj (i,x)) . ((proj (i,j)) . x)) . k = x /. k by A3, A6, A9, FINSEQ_7:10;
hence x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k by A5, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

hence x = (reproj (i,x)) . ((proj (i,j)) . x) by A1, FINSEQ_1:13; :: thesis: verum