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 ;
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 ;
A4: len (f /^ n) = (len f) - n by ;
then A5: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by
.= len f ;
A6: dom (f | n) = Seg n by ;
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 ;
A9: 1 <= m by ;
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 ;
then A11: n in dom f by ;
A12: m in Seg n by ;
hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by
.= f . m by ;
:: 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 ;
then A14: 1 <= k by XREAL_1:19;
k <= len (f /^ n) by ;
then A15: k in dom (f /^ n) by ;
thus ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by
.= f . (k + n) by
.= 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 ; :: thesis: verum
end;
end;
end;
hence (f | n) ^ (f /^ n) = f ; :: thesis: verum