let p be FinSequence; :: thesis: for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*>

let x, y, z be set ; :: thesis: ( p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> implies p = <*z,y,x*> )
assume that
A1: p is one-to-one and
A2: rng p = {x,y,z} and
A3: ( x <> y & y <> z & z <> x ) ; :: thesis: ( p = <*x,y,z*> or p = <*x,z,y*> or p = <*y,x,z*> or p = <*y,z,x*> or p = <*z,x,y*> or p = <*z,y,x*> )
A4: len p = 3 by ;
then A5: dom p = {1,2,3} by ;
then A6: 2 in dom p by ENUMSET1:def 1;
then A7: p . 2 in rng p by FUNCT_1:def 3;
A8: 3 in dom p by ;
then A9: p . 3 in rng p by FUNCT_1:def 3;
A10: 1 in dom p by ;
then p . 1 in rng p by FUNCT_1:def 3;
then ( ( p . 1 = x & p . 2 = x & p . 3 = x ) or ( p . 1 = x & p . 2 = x & p . 3 = y ) or ( p . 1 = x & p . 2 = x & p . 3 = z ) or ( p . 1 = x & p . 2 = y & p . 3 = x ) or ( p . 1 = x & p . 2 = y & p . 3 = y ) or ( p . 1 = x & p . 2 = y & p . 3 = z ) or ( p . 1 = x & p . 2 = z & p . 3 = x ) or ( p . 1 = x & p . 2 = z & p . 3 = y ) or ( p . 1 = x & p . 2 = z & p . 3 = z ) or ( p . 1 = y & p . 2 = x & p . 3 = x ) or ( p . 1 = y & p . 2 = x & p . 3 = y ) or ( p . 1 = y & p . 2 = x & p . 3 = z ) or ( p . 1 = y & p . 2 = y & p . 3 = x ) or ( p . 1 = y & p . 2 = y & p . 3 = y ) or ( p . 1 = y & p . 2 = y & p . 3 = z ) or ( p . 1 = y & p . 2 = z & p . 3 = x ) or ( p . 1 = y & p . 2 = z & p . 3 = y ) or ( p . 1 = y & p . 2 = z & p . 3 = z ) or ( p . 1 = z & p . 2 = x & p . 3 = x ) or ( p . 1 = z & p . 2 = x & p . 3 = y ) or ( p . 1 = z & p . 2 = x & p . 3 = z ) or ( p . 1 = z & p . 2 = y & p . 3 = x ) or ( p . 1 = z & p . 2 = y & p . 3 = y ) or ( p . 1 = z & p . 2 = y & p . 3 = z ) or ( p . 1 = z & p . 2 = z & p . 3 = x ) or ( p . 1 = z & p . 2 = z & p . 3 = y ) or ( p . 1 = z & p . 2 = z & p . 3 = z ) ) by ;
hence ( p = <*x,y,z*> or p = <*x,z,y*> or p = <*y,x,z*> or p = <*y,z,x*> or p = <*z,x,y*> or p = <*z,y,x*> ) by ; :: thesis: verum