let A, B be set ; :: thesis: for R being Relation holds R | (A \ B) = (R | A) \ [:B,(rng R):]
let R be Relation; :: thesis: R | (A \ B) = (R | A) \ [:B,(rng R):]
set lh = R | (A \ B);
set rh = (R | A) \ [:B,(rng R):];
R | (A \ B) = (R | A) \ (R | B) by RELAT_1:80
.= (R | A) \ (R /\ [:B,(rng R):]) by RELAT_1:67
.= (((R | A) null R) \ R) \/ ((R | A) \ [:B,(rng R):]) by XBOOLE_1:54
.= {} \/ ((R | A) \ [:B,(rng R):]) ;
hence R | (A \ B) = (R | A) \ [:B,(rng R):] ; :: thesis: verum