let i, n be Element of NAT ; :: thesis: for t being Element of n -tuples_on NAT holds (n proj i) . t = t . i
let t be Element of n -tuples_on NAT; :: thesis: (n proj i) . t = t . i
dom (n proj i) = n -tuples_on NAT by Th35;
hence (n proj i) . t = t . i by CARD_3:def 16; :: thesis: verum