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 = f by Th10;
f /^ n = {} by A1, Th15;
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

set g = f | n;
A4: len (f | n) = n by A3, Th12;
A5: len (f /^ n) = (len f) - n by A3, Th16;

A6: now

let m be Element of NAT ; :: thesis: ( m < len f implies ((f | n) ^ (f /^ n)) . m = f . m )
assume A7: 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 A8: m in n by NAT_1:45;
hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A4, AFINSQ_1:def 4
.= f . m by A3, A8, Th11 ;
:: 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;
k < len (f /^ n) by A5, A7, XREAL_1:11;
then A9: k in dom (f /^ n) by NAT_1:45;
m = (len (f | n)) + k by A4;
hence ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A9, AFINSQ_1:def 4
.= f . (k + n) by A9, Def2
.= f . m ;
:: thesis: verum

end;

end;

end;

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

end;

len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A5, A4, AFINSQ_1:20
.= len f ;
hence (f | n) ^ (f /^ n) = f by A6, AFINSQ_1:11; :: thesis: verum

end;

end;

end;

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