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