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