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 )
dom f = Seg (len f) by FINSEQ_1:def 3;
then A1: Sgm ((dom f) \ {n}) is one-to-one by FINSEQ_3:92, XBOOLE_1:36;
assume f is one-to-one ; :: thesis: Del (f,n) is one-to-one
hence Del (f,n) is one-to-one by A1; :: thesis: verum