let x, y be set ; :: thesis: for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds
( f . 1 = y & f . 2 = x )
let f be FinSequence; :: thesis: ( rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) implies ( f . 1 = y & f . 2 = x ) )
assume A1: ( rng f = {x,y} & len f = 2 ) ; :: thesis: ( ( f . 1 = x & f . 2 = y ) or ( f . 1 = y & f . 2 = x ) )
then 1 in Seg (len f) by FINSEQ_1:3;
then 1 in dom f by FINSEQ_1:def 3;
then A2: f . 1 in rng f by FUNCT_1:def 5;
2 in Seg (len f) by A1, FINSEQ_1:3;
then 2 in dom f by FINSEQ_1:def 3;
then A3: f . 2 in rng f by FUNCT_1:def 5;

A4: now

assume A5: ( f . 1 = x & f . 2 = x ) ; :: thesis: ( f . 1 = x & f . 2 = y )
y in rng f by A1, TARSKI:def 2;
then consider z being set such that
A6: ( z in dom f & y = f . z ) by FUNCT_1:def 5;
A7: z in Seg (len f) by A6, FINSEQ_1:def 3;
reconsider nz = z as Element of NAT by A6;
A8: ( 1 <= nz & nz <= len f ) by A7, FINSEQ_1:3;

per cases ( nz = 1 or nz = 1 + 1 ) by A1, A8, NAT_1:9;

suppose nz = 1 ; :: thesis: ( f . 1 = x & f . 2 = y )

hence ( f . 1 = x & f . 2 = y ) by A5, A6; :: thesis: verum

end;

suppose nz = 1 + 1 ; :: thesis: ( f . 1 = x & f . 2 = y )

hence ( f . 1 = x & f . 2 = y ) by A5, A6; :: thesis: verum

end;

end;

end;

now

assume A9: ( f . 1 = y & f . 2 = y ) ; :: thesis: ( f . 1 = x & f . 2 = y )
x in rng f by A1, TARSKI:def 2;
then consider z being set such that
A10: ( z in dom f & x = f . z ) by FUNCT_1:def 5;
A11: z in Seg (len f) by A10, FINSEQ_1:def 3;
reconsider nz = z as Element of NAT by A10;
A12: ( 1 <= nz & nz <= len f ) by A11, FINSEQ_1:3;

per cases ( nz = 1 or nz = 1 + 1 ) by A1, A12, NAT_1:9;

suppose nz = 1 ; :: thesis: ( f . 1 = x & f . 2 = y )

hence ( f . 1 = x & f . 2 = y ) by A9, A10; :: thesis: verum

end;

suppose nz = 1 + 1 ; :: thesis: ( f . 1 = x & f . 2 = y )

hence ( f . 1 = x & f . 2 = y ) by A9, A10; :: thesis: verum

end;

end;

end;

hence ( ( f . 1 = x & f . 2 = y ) or ( f . 1 = y & f . 2 = x ) ) by A1, A2, A3, A4, TARSKI:def 2; :: thesis: verum