let X, Y, Z be set ; :: thesis: for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
let f be Function; :: thesis: Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
thus Z |` <:f,X,Y:> = Z |` (Y |` (f | X)) by RELAT_1:109
.= (Z /\ Y) |` (f | X) by RELAT_1:96
.= <:f,X,(Z /\ Y):> by RELAT_1:109 ; :: thesis: verum