thus dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1; :: thesis: dom proj2 = REAL 2
hence dom proj2 = REAL 2 by EUCLID:25; :: thesis: verum