let i, j 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;
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; :: thesis: ( k in dom x implies x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k )
assume A3: k in dom x ; :: thesis: 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;
per cases ( k = i or k <> i ) ;
suppose A6: 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 A2, A4, A5, FINSEQ_7:8;
hence x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k by A6, 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 A2, A4, A5, FINSEQ_7:10;
hence x . k = ((reproj (i,x)) . ((proj (i,j)) . x)) . k by A3, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
hence x = (reproj (i,x)) . ((proj (i,j)) . x) by A1, FINSEQ_1:13; :: thesis: verum