A1: (2 * n) - n = n ;
1 * n < 2 * n by XREAL_1:68;
hence Op-Right (s,n) is Element of n -tuples_on D by A1, Th2; :: thesis: verum