let n be Nat; :: thesis: for M being FinSequence st len M = n + 1 holds
len (Del M,(n + 1)) = n
let M be FinSequence; :: thesis: ( len M = n + 1 implies len (Del M,(n + 1)) = n )
assume A1: len M = n + 1 ; :: thesis: len (Del M,(n + 1)) = n
then n + 1 in Seg (len M) by FINSEQ_1:6;
then n + 1 in dom M by FINSEQ_1:def 3;
hence len (Del M,(n + 1)) = n by A1, FINSEQ_3:118; :: thesis: verum