set D = dom P;
set C = rng P;
set XX = X \/ (rng P);
(P " ((rng P) null X)) \ (P " (X \/ (rng P))) = {} ;
then P " (rng P) c= P " (X \/ (rng P)) by Th29;
then ( dom P c= P " (X \/ (rng P)) & P " (X \/ (rng P)) c= dom P ) by RELAT_1:134, RELAT_1:132;
hence (P " (X \/ (rng P))) \+\ (dom P) is empty by XBOOLE_0:def 10, Th29; :: thesis: verum