let Y, X be set ; :: thesis: for f, g being Function st f c= g holds
(Y | f) | X c= (Y | g) | X
let f, g be Function; :: thesis: ( f c= g implies (Y | f) | X c= (Y | g) | X )
assume f c= g ; :: thesis: (Y | f) | X c= (Y | g) | X
then Y | f c= Y | g by RELAT_1:132;
hence (Y | f) | X c= (Y | g) | X by RELAT_1:105; :: thesis: verum