reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
S . i9 = S . i ;
hence S . i is Element of T ; :: thesis: verum