let I1, I2 be Integer; :: thesis: ( A in (Seq_of_ind T) . (I1 + 1) & not A in (Seq_of_ind T) . I1 & A in (Seq_of_ind T) . (I2 + 1) & not A in (Seq_of_ind T) . I2 implies I1 = I2 )
assume that
A6: A in (Seq_of_ind T) . (I1 + 1) and
A7: not A in (Seq_of_ind T) . I1 and
A8: A in (Seq_of_ind T) . (I2 + 1) and
A9: not A in (Seq_of_ind T) . I2 ; :: thesis: I1 = I2
( I1 + 1 in dom (Seq_of_ind T) & I2 + 1 in dom (Seq_of_ind T) ) by A6, A8, FUNCT_1:def 2;
then reconsider i11 = I1 + 1, i21 = I2 + 1 as Element of NAT ;
A10: I1 <= I2

proof

assume I1 > I2 ; :: thesis: contradiction
then A11: I1 >= i21 by INT_1:7;
then reconsider i1 = I1 as Element of NAT by INT_1:3;
(Seq_of_ind T) . i21 c= (Seq_of_ind T) . i1 by A11, PROB_1:def 5;
hence contradiction by A7, A8; :: thesis: verum

end;

I2 <= I1

proof

assume I1 < I2 ; :: thesis: contradiction
then A12: I2 >= i11 by INT_1:7;
then reconsider i2 = I2 as Element of NAT by INT_1:3;
(Seq_of_ind T) . i11 c= (Seq_of_ind T) . i2 by A12, PROB_1:def 5;
hence contradiction by A6, A9; :: thesis: verum

end;

hence I1 = I2 by A10, XXREAL_0:1; :: thesis: verum