let I1, I2 be Integer; :: thesis: ( G c= (Seq_of_ind T) . (I1 + 1) & - 1 <= I1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I1 <= i ) & G c= (Seq_of_ind T) . (I2 + 1) & - 1 <= I2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I2 <= i ) implies I1 = I2 )
assume ( G c= (Seq_of_ind T) . (I1 + 1) & - 1 <= I1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I1 <= i ) & G c= (Seq_of_ind T) . (I2 + 1) & - 1 <= I2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
I2 <= i ) ) ; :: thesis: I1 = I2
then ( I2 <= I1 & I1 <= I2 ) ;
hence I1 = I2 by XXREAL_0:1; :: thesis: verum