len (f | i) = min ((len f),i) by FINSEQ_2:21;
then i + j >= len (f | i) by XXREAL_0:17, NAT_1:12;
then reconsider k = (i + j) - (len (f | i)) as Element of NAT by NAT_1:21;
(f | i) | (i + j) = (f | i) | ((len (f | i)) + k) ;
hence (f | i) | (i + j) = f | i ; :: thesis: verum