defpred S₁[ Nat] means A in (Seq_of_ind T) . $1;
A2: ex n being Nat st S₁[n] by A1;
consider MIN being Nat such that
A3: S₁[MIN] and
A4: for n being Nat st S₁[n] holds
MIN <= n from NAT_1:sch 5(A2);
take I = MIN - 1; :: thesis: ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I )

now :: thesis: not A in (Seq_of_ind T) . I

assume A5: A in (Seq_of_ind T) . I ; :: thesis: contradiction
then I in dom (Seq_of_ind T) by FUNCT_1:def 2;
then reconsider i = I as Element of NAT ;
MIN <= i by A4, A5;
then MIN < i + 1 by NAT_1:13;
hence contradiction ; :: thesis: verum

end;

hence ( A in (Seq_of_ind T) . (I + 1) & not A in (Seq_of_ind T) . I ) by A3; :: thesis: verum