let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j being Nat holds
( f is one-to-one iff Swap (f,i,j) is one-to-one )
let f be FinSequence of D; :: thesis: for i, j being Nat holds
( f is one-to-one iff Swap (f,i,j) is one-to-one )
let i, j be Nat; :: thesis: ( f is one-to-one iff Swap (f,i,j) is one-to-one )
thus ( f is one-to-one implies Swap (f,i,j) is one-to-one ) :: thesis: ( Swap (f,i,j) is one-to-one implies f is one-to-one )

proof

set ff = Swap (f,i,j);
A1: rng (Swap (f,i,j)) = rng f by FINSEQ_7:22;
assume f is one-to-one ; :: thesis: Swap (f,i,j) is one-to-one
then A2: card (rng f) = len f by FINSEQ_4:62;
len (Swap (f,i,j)) = len f by FINSEQ_7:18;
hence Swap (f,i,j) is one-to-one by A2, A1, FINSEQ_4:62; :: thesis: verum

end;

assume Swap (f,i,j) is one-to-one ; :: thesis: f is one-to-one
then card (rng (Swap (f,i,j))) = len (Swap (f,i,j)) by FINSEQ_4:62;
then card (rng f) = len (Swap (f,i,j)) by FINSEQ_7:22;
then card (rng f) = len f by FINSEQ_7:18;
hence f is one-to-one by FINSEQ_4:62; :: thesis: verum