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 set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [a,b] in R * (S | X) iff [a,b] in R * S )
let b be set ; :: thesis: ( [a,b] in R * (S | X) iff [a,b] in R * S )
R * (S | X) c= R * S by Th48, Th88;
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 set such that
A2: [a,c] in R and
A3: [c,b] in S by Def8;
c in rng R by A2, Def5;
then c in X by A1, Th86;
then [c,b] in S | X by A3, Def11;
hence [a,b] in R * (S | X) by A2, Def8; :: thesis: verum