let i be Nat; :: thesis: for f being FinSequence holds len (f /^ i) <= len f
let f be FinSequence; :: thesis: len (f /^ i) <= len f

per cases ( i <= len f or len f < i ) ;

suppose i <= len f ; :: thesis: len (f /^ i) <= len f

then len (f /^ i) = (len f) - i by RFINSEQ:def 1;
then (len (f /^ i)) + i = len f ;
hence len (f /^ i) <= len f by NAT_1:11; :: thesis: verum

end;

suppose len f < i ; :: thesis: len (f /^ i) <= len f

then f /^ i = {} by RFINSEQ:def 1;
hence len (f /^ i) <= len f ; :: thesis: verum

end;

end;