for X, Y being set
for f being Function st X c= Y holds
( (f | X) | Y = f | X & (f | Y) | X = f | X ) by RELAT_1:73, RELAT_1:74;