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

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