A1: rng f c= V by RELAT_1:def 19;
A3: rng (f +* (x,y)) c= (rng f) \/ {y} by Th102;
(rng f) \/ {y} c= V by A1, XBOOLE_1:8;
hence rng (f +* (x,y)) c= V by A3, XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum