let f be FinSequence; :: thesis: for i being Nat st i >= len f holds
f /^ i = {}
let i be Nat; :: thesis: ( i >= len f implies f /^ i = {} )
assume A1: i >= len f ; :: thesis: f /^ i = {}

per cases ( i > len f or i = len f ) by A1, XXREAL_0:1;

suppose i > len f ; :: thesis: f /^ i = {}

hence f /^ i = {} by RFINSEQ:def 1; :: thesis: verum

end;

suppose A2: i = len f ; :: thesis: f /^ i = {}

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

end;

end;