L0: (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 L0, LM002B; :: thesis: verum