let i be Nat; :: thesis: for f being FinSequence st len f <= i holds
f /^ i is empty
let f be FinSequence; :: thesis: ( len f <= i implies f /^ i is empty )
assume A1: len f <= i ; :: thesis: f /^ i is empty

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

suppose len f = i ; :: thesis: f /^ i is empty

then len (f /^ i) = (len f) - (len f) by RFINSEQ:def 1
.= 0 ;
hence f /^ i is empty ; :: thesis: verum

end;

suppose len f <> i ; :: thesis: f /^ i is empty

then len f < i by A1, XXREAL_0:1;
hence f /^ i is empty by RFINSEQ:def 1; :: thesis: verum

end;

end;