let m, n be Nat; :: thesis: for f being FinSequence st len f = m + 1 & n in dom f holds
len (Del (f,n)) = m
let f be FinSequence; :: thesis: ( len f = m + 1 & n in dom f implies len (Del (f,n)) = m )
assume that
A1: len f = m + 1 and
A2: 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 A2, Th102;
hence len (Del (f,n)) = m by A1; :: thesis: verum