let m, n be natural number ; :: 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, Th113;
hence len (Del f,n) = m by A1; :: thesis: verum