let f be XFinSequence; :: thesis: for n being Element of NAT holds (f | n) ^ (f /^ n) = f
let n be Element of 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 = {} by TH80e;
f | n = f by A1, Lm4;
hence (f | n) ^ (f /^ n) = f by A2, AFINSQ_1:32; :: 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, TH80b;
set g = f | n;
A5: len (f | n) = n by A3, TH80;
then A6: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A4, AFINSQ_1:20
.= len f ;

now

let m be Element of NAT ; :: thesis: ( m < len f implies ((f | n) ^ (f /^ n)) . m = f . m )
assume A8: m < len f ; :: thesis: ((f | n) ^ (f /^ n)) . m = f . m

now

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

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

then A9: m in n by NAT_1:45;
thus ((f | n) ^ (f /^ n)) . m = (f | n) . m by A5, A9, AFINSQ_1:def 4
.= f . m by A3, A9, Th19 ; :: thesis: verum

end;

case 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;
A20: k < len (f /^ n) by A4, A8, XREAL_1:11;
A12: m = (len (f | n)) + k by A5;
A13: k in dom (f /^ n) by A20, NAT_1:45;
hence ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A12, AFINSQ_1:def 4
.= f . (k + n) by 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, AFINSQ_1:11; :: thesis: verum

end;

end;

end;

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