let X be set ; for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
let R, S be Relation; ( rng R c= dom (S | X) implies R * (S | X) = R * S )
assume A1:
rng R c= dom (S | X)
; R * (S | X) = R * S
let a be object ; RELAT_1:def 2 for b being object holds
( [a,b] in R * (S | X) iff [a,b] in R * S )
let b be object ; ( [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 )
; ( [a,b] in R * S implies [a,b] in R * (S | X) )
assume
[a,b] in R * S
; [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; verum