let D be non empty set ; :: thesis: for f being FinSequence of D holds f /^ (len f) = {}
let f be FinSequence of D; :: thesis: f /^ (len f) = {}
len (f /^ (len f)) = (len f) - (len f) by Def2
.= 0 ;
hence f /^ (len f) = {} ; :: thesis: verum