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