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

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