let X, Y 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:101;
hence (Y |` f) | X c= (Y |` g) | X by RELAT_1:76; :: thesis: verum