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