thus L . i is Element of m -tuples_on D ; :: thesis: verum