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