let h be non constant standard special_circular_sequence; :: thesis: for i1, i2 being 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 Nat; :: thesis: ( 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 implies i1 = i2 )
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len h ; :: thesis: ( not 1 <= i2 or not i2 + 1 <= len h or not h . i1 = h . i2 or i1 = i2 )
A3: i1 < len h by A2, NAT_1:13;
assume that
A4: 1 <= i2 and
A5: i2 + 1 <= len h and
A6: h . i1 = h . i2 ; :: thesis: i1 = i2
A7: i2 < len h by A5, NAT_1:13;
then A8: i2 in dom h by A4, FINSEQ_3:25;
assume A9: i1 <> i2 ; :: thesis: contradiction
A10: now :: thesis: h /. i1 <> h /. i2
per cases ( i1 < i2 or i2 < i1 ) by A9, XXREAL_0:1;
suppose i1 < i2 ; :: thesis: h /. i1 <> h /. i2
hence h /. i1 <> h /. i2 by A1, A7, GOBOARD7:36; :: thesis: verum
end;
suppose i2 < i1 ; :: thesis: h /. i1 <> h /. i2
hence h /. i1 <> h /. i2 by A4, A3, GOBOARD7:36; :: thesis: verum
end;
end;
end;
i1 in dom h by A1, A3, FINSEQ_3:25;
then h /. i1 = h . i2 by A6, PARTFUN1:def 6
.= h /. i2 by A8, PARTFUN1:def 6 ;
hence contradiction by A10; :: thesis: verum