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

assume f is one-to-one ; :: thesis: Swap f,i,j is one-to-one
then A1: card (rng f) = len f by FINSEQ_4:77;
set ff = Swap f,i,j;
( len (Swap f,i,j) = len f & rng (Swap f,i,j) = rng f ) by FINSEQ_7:20, FINSEQ_7:24;
hence Swap f,i,j is one-to-one by A1, FINSEQ_4:77; :: 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:77;
then card (rng f) = len (Swap f,i,j) by FINSEQ_7:24;
then card (rng f) = len f by FINSEQ_7:20;
hence f is one-to-one by FINSEQ_4:77; :: thesis: verum