dom <.gen_R^1.] = REAL by Th64, FUNCT_2:def 1;