let p be FinSequence; :: thesis:
let x, y, z be set ; :: thesis:
assume that
A1: p is one-to-one and
A2: rng p = {x,y,z} and
A3: ( x <> y & y <> z & z <> x ) ; :: thesis:
A4: len p = 3 by A1, A2, A3, FINSEQ_3:110;
then dom p = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
then A5: ( 1 in dom p & 2 in dom p & 3 in dom p ) by ENUMSET1:def 1;
then ( p . 1 in rng p & p . 2 in rng p & p . 3 in rng p & 1 <> 2 & 2 <> 3 & 3 <> 1 ) by FUNCT_1:def 5;
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 ) ) & p . 1 <> p . 2 & p . 2 <> p . 3 & p . 3 <> p . 1 ) by A1, A2, A5, ENUMSET1:def 1, FUNCT_1:def 8;
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 A4, FINSEQ_1:62; :: thesis: