let D be non empty 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;

now :: thesis: ( ( len f < n & (f | n) ^ (f /^ n) = f ) or ( n <= len f & (f | n) ^ (f /^ n) = f ) )

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

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

then ( f /^ n = <*> D & f | n = f ) by Def1, Lm3;
hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; :: thesis: verum

end;

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

A2: dom f = Seg (len f) by FINSEQ_1:def 3;
A3: len (f | n) = n by A1, FINSEQ_1:59;
A4: len (f /^ n) = (len f) - n by A1, Def1;
then A5: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A3, FINSEQ_1:22
.= len f ;
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)) . m = f . m )
assume A7: m in dom f ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m
then A8: m <= len f by A2, FINSEQ_1:1;
A9: 1 <= m by A2, A7, FINSEQ_1:1;

now :: thesis: ( ( m <= n & ((f | n) ^ (f /^ n)) . m = f . m ) or ( n < m & ((f | n) ^ (f /^ n)) . m = f . m ) )

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

case A10: m <= n ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

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

end;

case A13: n < m ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

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 A14: 1 <= k by XREAL_1:19;
k <= len (f /^ n) by A4, A8, XREAL_1:9;
then A15: k in dom (f /^ n) by A14, FINSEQ_3:25;
thus ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A3, A5, A8, A13, FINSEQ_1:24
.= f . (k + n) by A1, A15, Def1
.= f . m ; :: thesis: verum

end;

end;

end;

hence ((f | n) ^ (f /^ n)) . m = f . m ; :: thesis: verum

end;

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

end;

end;

end;

hence (f | n) ^ (f /^ n) = f ; :: thesis: verum