theorem :: FOMODEL0:11

for Y being set
for i being Nat holds i -tuples_on Y = Funcs ((Seg i),Y) by Lm7;