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:4;
then n + 1 in dom M by FINSEQ_1:def 3;
hence len (Del (M,(n + 1))) = n by A1, FINSEQ_3:109; :: thesis: verum