let h be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds
i1 = i2
let i1, i2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 implies i1 = i2 )
assume A1: ( 1 <= i1 & i1 + 1 <= len h ) ; :: thesis: ( not 1 <= i2 or not i2 + 1 <= len h or not h . i1 = h . i2 or i1 = i2 )
assume A2: ( 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 ) ; :: thesis: i1 = i2
assume A3: i1 <> i2 ; :: thesis: contradiction
A4: ( i1 < len h & i2 < len h ) by A1, A2, NAT_1:13;
then A5: ( i1 in dom h & i2 in dom h ) by A1, A2, FINSEQ_3:27;
then A6: h /. i1 = h . i2 by A2, PARTFUN1:def 8
.= h /. i2 by A5, PARTFUN1:def 8 ;

now

per cases ( i1 < i2 or i2 < i1 ) by A3, XXREAL_0:1;

suppose i1 < i2 ; :: thesis: h /. i1 <> h /. i2

hence h /. i1 <> h /. i2 by A1, A4, GOBOARD7:38; :: thesis: verum

end;

suppose i2 < i1 ; :: thesis: h /. i1 <> h /. i2

hence h /. i1 <> h /. i2 by A2, A4, GOBOARD7:38; :: thesis: verum

end;

end;

end;

hence contradiction by A6; :: thesis: verum