consider E being Function such that
A1: ( dom E c= X & rng E c= Y ) by Lm1;
reconsider E = E as Relation of X,Y by A1, RELSET_1:4;
take E ; :: thesis: E is Function-like
thus E is Function-like ; :: thesis: verum