let f be FinSequence; :: thesis: f /^ (len f) = {}
len (f /^ (len f)) = (len f) - (len f) by Def1
.= 0 ;
hence f /^ (len f) = {} ; :: thesis: verum