A1: 1 * n <= 2 * n by XREAL_1:68;
len s = 2 * n by CARD_1:def 7;
then len (Op-Left (s,n)) = n by A1, FINSEQ_1:59;
hence Op-Left (s,n) is Element of n -tuples_on D by FINSEQ_2:92; :: thesis: verum