let p be FinSequence; for x, y being object st p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> holds
p = <*y,x*>
let x, y be object ; ( p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> implies p = <*y,x*> )
assume that
A1:
p is one-to-one
and
A2:
rng p = {x,y}
and
A3:
x <> y
; ( p = <*x,y*> or p = <*y,x*> )
A4:
len p = 2
by A1, A2, A3, Th96;
then A5:
dom p = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A6:
2 in dom p
by TARSKI:def 2;
then A7:
p . 2 in rng p
by FUNCT_1:def 3;
A8:
1 in dom p
by A5, TARSKI:def 2;
then
p . 1 in rng p
by FUNCT_1:def 3;
then
( ( p . 1 = x & p . 2 = x ) or ( p . 1 = x & p . 2 = y ) or ( p . 1 = y & p . 2 = x ) or ( p . 1 = y & p . 2 = y ) )
by A2, A7, TARSKI:def 2;
hence
( p = <*x,y*> or p = <*y,x*> )
by A1, A4, A8, A6, FINSEQ_1:44; verum