n + m >= n + 0 by XREAL_1:6;
then len f >= n by CARD_1:def 7;
then Segm n c= Segm (len f) by NAT_1:39;
then n = Segm (len (f | n)) by RELAT_1:62;
hence f | n is n -element by CARD_1:def 7; :: thesis: verum