let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 (f ^ g) or not r <= 0 )
assume r in rng (f ^ g) ; :: thesis: not r <= 0
then r in (rng f) \/ (rng g) by FINSEQ_1:31;
then ( r in rng f or r in rng g ) by XBOOLE_0:def 3;
hence not r <= 0 by PARTFUN3:def 1; :: thesis: verum