let k be Element of NAT ; :: thesis: for F being XFinSequence st k <= len F holds
len (F | k) = k
let F be XFinSequence; :: thesis: ( k <= len F implies len (F | k) = k )
assume A1: k <= len F ; :: thesis: len (F | k) = k

per cases ( k = len F or k < len F ) by A1, XXREAL_0:1;

suppose k = len F ; :: thesis: len (F | k) = k

then dom F = k ;
then ( F | k = F & dom F = k & len F = k ) by RELAT_1:98;
hence len (F | k) = k ; :: thesis: verum

end;

suppose k < len F ; :: thesis: len (F | k) = k

hence len (F | k) = k by AFINSQ_1:14; :: thesis: verum

end;

end;