reconsider i = i as Element of NAT by ORDINAL1:def 13;
B . g,i is Element of ;
hence B . g,i is Element of ; :: thesis: verum