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:104;
hence len (Del (f,i)) = (len f) -' 1 by NAT_D:34; :: thesis: verum