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

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

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

then A2: f /^ n = <*> D by Def2;
f | n = f by A1, Lm4;
hence (f | n) ^ (f /^ n) = f by A2, FINSEQ_1:47; :: thesis: verum

end;

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

then A4: ( len (f /^ n) = (len f) - n & ( for m being Element of NAT st m in dom (f /^ n) holds
(f /^ n) . m = f . (m + n) ) ) by Def2;
A5: len (f | n) = n by A3, FINSEQ_1:80;
then A6: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A4, FINSEQ_1:35
.= len f ;
A7: ( dom (f | n) = Seg n & dom f = dom f & dom (f /^ n) = dom (f /^ n) ) by A5, FINSEQ_1:def 3;
X: dom f = Seg (len f) by FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom f implies ((f | n) ^ (f /^ n)) . m = f . m )
assume m in dom f ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m
then A8: ( 1 <= m & m <= len f ) by X, FINSEQ_1:3;

now

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

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

then A9: ( m in Seg n & 1 <= n ) by A8, FINSEQ_1:3, XXREAL_0:2;
then A10: n in dom f by A3, FINSEQ_3:27;
thus ((f | n) ^ (f /^ n)) . m = (f | n) . m by A7, A9, FINSEQ_1:def 7
.= f . m by A9, A10, Th19 ; :: thesis: verum

end;

case A11: 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 A11, NAT_1:13;
then A12: 1 <= k by XREAL_1:21;
k <= len (f /^ n) by A4, A8, XREAL_1:11;
then A13: k in dom (f /^ n) by A12, FINSEQ_3:27;
thus ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A5, A6, A8, A11, FINSEQ_1:37
.= f . (k + n) by A3, A13, Def2
.= 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 A6, FINSEQ_2:10; :: thesis: verum

end;

end;

end;

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