let n be Nat; :: thesis: for f being FinSequence st f is one-to-one holds
Del (f,n) is one-to-one
let f be FinSequence; :: thesis: ( f is one-to-one implies Del (f,n) is one-to-one )
Sgm ((dom f) \ {n}) is one-to-one by FINSEQ_3:92;
hence ( f is one-to-one implies Del (f,n) is one-to-one ) ; :: thesis: verum