( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= REAL & rng q c= REAL ) by AFINSQ_1:26, VALUED_0:def 3;
hence p ^ q is real-valued by VALUED_0:def 3, XBOOLE_1:8; :: thesis: verum