reconsider i = i as Element of NAT by ORDINAL1:def 12;
T . i is Element of divs A ;
hence T . i is Division of A by INTEGRA1:def 3; :: thesis: verum