let f be FinSequence; :: thesis: for n, m being natural number st len f = m + 1 & n in dom f holds
len (Del f,n) = m
let n, m be natural number ; :: thesis: ( len f = m + 1 & n in dom f implies len (Del f,n) = m )
assume A1: ( len f = m + 1 & n in dom f ) ; :: thesis: len (Del f,n) = m
ex k being Nat st
( len f = k + 1 & len (Del f,n) = k ) by A1, Th113;
hence len (Del f,n) = m by A1; :: thesis: verum