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