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;
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 or 3 = i ) & j <> 2 ) ; :: thesis: i = j
hence i = j by A8, Z2, A3, XXREAL_0:1, A1a; :: thesis: verum
end;
suppose ( ( 1 = j or 3 = j ) & i <> 2 ) ; :: thesis: i = j
hence i = j by A8, Z2, XXREAL_0:1, A1, A2; :: thesis: verum
end;
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 ) ) ; :: thesis: i = j
hence i = j by Z2, Z1, A12; :: thesis: verum
end;
end;