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