consider k being Nat such that
A1: N c= Seg k by Th43;
len (Sgm N) = card N by A1, FINSEQ_3:44;
hence Sgm N is Element of (card N) -tuples_on NAT by FINSEQ_2:110; :: thesis: verum