ex k being Nat st N c= Seg k by Th43;
then len (Sgm N) = card N by FINSEQ_3:39;
hence Sgm N is Element of (card N) -tuples_on NAT by FINSEQ_2:92; :: thesis: verum