let R be Relation; :: thesis: R .: (dom R) = rng R
thus R .: (dom R) c= rng R by Th105; :: according to XBOOLE_0:def 10 :: thesis: rng R c= R .: (dom R)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng R or y in R .: (dom R) )
assume y in rng R ; :: thesis: y in R .: (dom R)
then consider x being object such that
A1: [x,y] in R by XTUPLE_0:def 13;
x in dom R by A1, XTUPLE_0:def 12;
hence y in R .: (dom R) by A1, Def11; :: thesis: verum