let X, Y be set ; :: thesis: for R being Relation of X,Y holds

( R .: (R " Y) = rng R & R " (R .: X) = dom R )

let R be Relation of X,Y; :: thesis: ( R .: (R " Y) = rng R & R " (R .: X) = dom R )

( R " Y = dom R & R .: X = rng R ) by Th22;

hence ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) by RELAT_1:113, RELAT_1:134; :: thesis: verum

( R .: (R " Y) = rng R & R " (R .: X) = dom R )

let R be Relation of X,Y; :: thesis: ( R .: (R " Y) = rng R & R " (R .: X) = dom R )

( R " Y = dom R & R .: X = rng R ) by Th22;

hence ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) by RELAT_1:113, RELAT_1:134; :: thesis: verum