A1: rng (g +* h) c= (rng g) \/ (rng h) by Th18;
( rng g c= I & rng h c= I ) by RELAT_1:def 19;
then (rng g) \/ (rng h) c= I by XBOOLE_1:8;
then rng (g +* h) c= I by A1, XBOOLE_1:1;
hence g +* h is I -valued by RELAT_1:def 19; :: thesis: verum