let f be XFinSequence; :: thesis: for n being Nat st n >= len f holds
f /^ n = {}
let n be Nat; :: thesis: ( n >= len f implies f /^ n = {} )
assume n >= len f ; :: thesis: f /^ n = {}
then (len f) -' n = 0 by NAT_2:10;
then len (f /^ n) = 0 by Def2;
hence f /^ n = {} ; :: thesis: verum