let a, b be object ; :: thesis: ( a <> b implies <*a,b,a*> is almost-one-to-one )

assume Z1: a <> b ; :: thesis: <*a,b,a*> is almost-one-to-one

set f = <*a,b,a*>;

let i, j be Nat; :: according to JORDAN23:def 1 :: thesis: ( 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 ) ; :: thesis: 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;

assume Z1: a <> b ; :: thesis: <*a,b,a*> is almost-one-to-one

set f = <*a,b,a*>;

let i, j be Nat; :: according to JORDAN23:def 1 :: thesis: ( 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 ) ; :: thesis: 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;

end;