let p be FinSequence; :: thesis: for x, y being set st p is one-to-one & rng p = {x,y} & x <> y & not p = <*x,y*> holds
p = <*y,x*>
let x, y be set ; :: thesis: ( 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 ; :: thesis: ( p = <*x,y*> or p = <*y,x*> )
A4: len p = 2 by A1, A2, A3, Th107;
then dom p = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
then A5: ( 1 in dom p & 2 in dom p ) by TARSKI:def 2;
then ( p . 1 in rng p & p . 2 in rng p & 1 <> 2 ) by FUNCT_1:def 5;
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 ) ) & p . 1 <> p . 2 ) by A1, A2, A5, FUNCT_1:def 8, TARSKI:def 2;
hence ( p = <*x,y*> or p = <*y,x*> ) by A4, FINSEQ_1:61; :: thesis: verum