let a, b be object ; ( a <> b implies <*a,b,a*> is almost-one-to-one )
assume Z1:
a <> b
; <*a,b,a*> is almost-one-to-one
set f = <*a,b,a*>;
let i, j be Nat; JORDAN23:def 1 ( not i in dom <*a,b,a*> or not j in dom <*a,b,a*> or ( i = 1 & j = len <*a,b,a*> ) or ( i = len <*a,b,a*> & j = 1 ) or not <*a,b,a*> . i = <*a,b,a*> . j or i = j )
assume Z2:
( i in dom <*a,b,a*> & j in dom <*a,b,a*> & ( i <> 1 or j <> len <*a,b,a*> ) & ( i <> len <*a,b,a*> or j <> 1 ) & <*a,b,a*> . i = <*a,b,a*> . j )
; i = j
A8:
len <*a,b,a*> = 3
by FINSEQ_1:45;
then A1:
( 1 <= i & i <= 3 )
by FINSEQ_3:25, Z2;
A1a:
( 1 <= j & j <= 3 )
by FINSEQ_3:25, Z2, A8;
A12:
( <*a,b,a*> . 1 = a & <*a,b,a*> . 2 = b & <*a,b,a*> . 3 = a )
by FINSEQ_1:45;
( 1 = i or 1 < i )
by A1, XXREAL_0:1;
then
( 1 = i or 1 + 1 <= i )
by NAT_1:13;
then
( 1 = i or 2 = i or 2 < i )
by XXREAL_0:1;
then A2:
( 1 = i or 2 = i or 2 + 1 <= i )
by NAT_1:13;
( 1 = j or 1 < j )
by A1a, XXREAL_0:1;
then
( 1 = j or 1 + 1 <= j )
by NAT_1:13;
then
( 1 = j or 2 = j or 2 < j )
by XXREAL_0:1;
then A3:
( 1 = j or 2 = j or 2 + 1 <= j )
by NAT_1:13;
per cases then
( ( ( 1 = i or 3 = i ) & j <> 2 ) or ( ( 1 = j or 3 = j ) & i <> 2 ) or ( 1 = i & 2 = j ) or ( 2 = i & 1 = j ) or ( 2 = i & 2 = j ) or ( 2 = i & 3 = j ) or ( 3 = i & 2 = j ) )
by A1a, XXREAL_0:1, A1, A2;
suppose
( ( 1
= i & 2
= j ) or ( 2
= i & 1
= j ) or ( 2
= i & 2
= j ) or ( 2
= i & 3
= j ) or ( 3
= i & 2
= j ) )
;
i = jend; end;