theorem :: PARTFUN1:7

for X, Y being set
for f being Relation of X,Y holds f * (id Y) = f