take the E,F -respecting Function of X,Y ; :: thesis: the E,F -respecting Function of X,Y is E,F -respecting
thus the E,F -respecting Function of X,Y is E,F -respecting ; :: thesis: verum