let X, Y be set ; :: thesis: for f being Relation of X,Y holds f * (id Y) = f
let f be Relation of X,Y; :: thesis: f * (id Y) = f
rng f c= Y ;
hence f * (id Y) = f by RELAT_1:53; :: thesis: verum