let X be set ; :: thesis: for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
let R, S be Relation; :: thesis: ( rng R c= dom (S | X) implies R * (S | X) = R * S )
assume A1: rng R c= dom (S | X) ; :: thesis: R * (S | X) = R * S
let a be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [a,b] in R * (S | X) iff [a,b] in R * S )
let b be object ; :: thesis: ( [a,b] in R * (S | X) iff [a,b] in R * S )
R * (S | X) c= R * S by Th23, Th53;
hence ( [a,b] in R * (S | X) implies [a,b] in R * S ) ; :: thesis: ( [a,b] in R * S implies [a,b] in R * (S | X) )
assume [a,b] in R * S ; :: thesis: [a,b] in R * (S | X)
then consider c being object such that
A2: [a,c] in R and
A3: [c,b] in S by Def6;
c in rng R by A2, XTUPLE_0:def 13;
then c in X by A1, Th51;
then [c,b] in S | X by A3, Def9;
hence [a,b] in R * (S | X) by A2, Def6; :: thesis: verum