let X be set ; :: thesis: for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)
let R, S be Relation; :: thesis: ( rng R c= dom S implies R " X c= (R * S) " (S .: X) )
assume A1: rng R c= dom S ; :: thesis: R " X c= (R * S) " (S .: X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R " X or x in (R * S) " (S .: X) )
assume x in R " X ; :: thesis: x in (R * S) " (S .: X)
then consider Rx being object such that
A2: [x,Rx] in R and
A3: Rx in X by RELAT_1:def 14;
Rx in rng R by A2, XTUPLE_0:def 13;
then consider SRx being object such that
A4: [Rx,SRx] in S by A1, XTUPLE_0:def 12;
( SRx in S .: X & [x,SRx] in R * S ) by A2, A3, A4, RELAT_1:def 8, RELAT_1:def 13;
hence x in (R * S) " (S .: X) by RELAT_1:def 14; :: thesis: verum