let p be FinSequence; 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 ; ( 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 )
; ( 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 A1, A2, A3, FINSEQ_3:101;
then A5:
dom p = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
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 A5, ENUMSET1:def 1;
then A9:
p . 3 in rng p
by FUNCT_1:def 3;
A10:
1 in dom p
by A5, ENUMSET1:def 1;
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 A2, A7, A9, ENUMSET1:def 1;
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 A1, A4, A10, A6, A8, FINSEQ_1:45, FUNCT_1:def 4; verum