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 )

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

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
Swap (f,i,j) is one-to-one
; :: thesis: f is one-to-one
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;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

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