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

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