let Z, X, Y 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