let D be set ; :: thesis: for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f
let f be FinSequence of D; :: thesis: for n being Nat holds (f | n) ^ (f /^ n) = f
let n be Nat; :: thesis: (f | n) ^ (f /^ n) = f
set fn = f /^ n;

per cases ( len f < n or n <= len f ) ;

suppose len f < n ; :: thesis: (f | n) ^ (f /^ n) = f

then ( f /^ n = <*> D & f | n = f ) by RFINSEQ:def 1, RFINSEQlm3;
hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; :: thesis: verum

end;

suppose A1: n <= len f ; :: thesis: (f | n) ^ (f /^ n) = f

then A3: len (f | n) = n by FINSEQ_1:59;
A4: len (f /^ n) = (len f) - n by A1, RFINSEQ:def 1;
then A5: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A3, FINSEQ_1:22;
A6: dom (f | n) = Seg n by A3, FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom f holds
((f | n) ^ (f /^ n)) . m = f . m

let m be Nat; :: thesis: ( m in dom f implies ((f | n) ^ (f /^ n)) . b₁ = f . b₁ )
assume m in dom f ; :: thesis: ((f | n) ^ (f /^ n)) . b₁ = f . b₁
then A8: ( 1 <= m & m <= len f ) by FINSEQ_3:25;

per cases ( m <= n or n < m ) ;

suppose A10: m <= n ; :: thesis: ((f | n) ^ (f /^ n)) . b₁ = f . b₁

then 1 <= n by A8, XXREAL_0:2;
then A11: n in dom f by A1, FINSEQ_3:25;
A12: m in Seg n by A8, A10;
hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A6, FINSEQ_1:def 7
.= f . m by A12, A11, RFINSEQ6 ;
:: thesis: verum

end;

suppose A13: n < m ; :: thesis: ((f | n) ^ (f /^ n)) . b₁ = f . b₁

then max (0,(m - n)) = m - n by FINSEQ_2:4;
then reconsider k = m - n as Element of NAT by FINSEQ_2:5;
n + 1 <= m by A13, NAT_1:13;
then 1 <= k by XREAL_1:19;
then A15: k in dom (f /^ n) by A4, A8, XREAL_1:9, FINSEQ_3:25;
((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A3, A5, A8, A13, FINSEQ_1:24;
then ((f | n) ^ (f /^ n)) . m = f . (k + n) by A1, A15, RFINSEQ:def 1;
hence ((f | n) ^ (f /^ n)) . m = f . m ; :: thesis: verum

end;

end;

end;

hence (f | n) ^ (f /^ n) = f by A5, FINSEQ_2:9; :: thesis: verum

end;

end;