let f be FinSequence; :: thesis: for i being Nat st i in dom f holds
len (Del f,i) = (len f) -' 1
let i be Nat; :: thesis: ( i in dom f implies len (Del f,i) = (len f) -' 1 )
assume i in dom f ; :: thesis: len (Del f,i) = (len f) -' 1
then ex m being Nat st
( len f = m + 1 & len (Del f,i) = m ) by FINSEQ_3:113;
hence len (Del f,i) = (len f) -' 1 by NAT_D:34; :: thesis: verum