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