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