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