let X be set ; :: thesis: for P being Relation holds P | ((dom P) \ X) = P \ [:X,(rng P):]
let P be Relation; :: thesis: P | ((dom P) \ X) = P \ [:X,(rng P):]
set A = dom P;
set B = rng P;
set C = [:((dom P) \ X),(rng P):];
P \ [:(dom P),(rng P):] = {} ;
then reconsider P = P as Subset of [:(dom P),(rng P):] by Th29;
( (P \ ((P \/ [:(dom P),(rng P):]) \ [:((dom P) \ X),(rng P):])) \+\ (P /\ [:((dom P) \ X),(rng P):]) = {} & ([:(dom P),(rng P):] \ (([:(dom P),(rng P):] \/ {}) \ [:X,(rng P):])) \+\ ([:(dom P),(rng P):] /\ [:X,(rng P):]) = {} ) ;
then A1: ( P \ (([:(dom P),(rng P):] null P) \ [:((dom P) \ X),(rng P):]) = P /\ [:((dom P) \ X),(rng P):] & [:(dom P),(rng P):] \ ([:(dom P),(rng P):] \ [:X,(rng P):]) = [:(dom P),(rng P):] /\ [:X,(rng P):] ) by Th29;
P | ((dom P) \ X) = P \ ([:(dom P),(rng P):] /\ [:X,(rng P):]) by A1, ZFMISC_1:102
.= (P \ [:(dom P),(rng P):]) \/ (P \ [:X,(rng P):]) by XBOOLE_1:54
.= {} \/ (P \ [:X,(rng P):]) ;
hence P | ((dom P) \ X) = P \ [:X,(rng P):] ; :: thesis: verum