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
A5: A in (Seq_of_ind T) . (I1 + 1) and
A6: not A in (Seq_of_ind T) . I1 and
A7: A in (Seq_of_ind T) . (I2 + 1) and
A8: 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 A5, A7, FUNCT_1:def 2;
then reconsider i11 = I1 + 1, i21 = I2 + 1 as Element of NAT ;
A9: I1 <= I2

proof

assume I1 > I2 ; :: thesis: contradiction
then A10: 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 A10, PROB_1:def 5;
hence contradiction by A6, A7; :: thesis: verum

end;

I2 <= I1

proof

assume I1 < I2 ; :: thesis: contradiction
then A11: 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 A11, PROB_1:def 5;
hence contradiction by A5, A8; :: thesis: verum

end;

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