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