0 *' = 0 by Th4;