take the Function of X,(Funcs (Y,Z)) ; :: thesis: the Function of X,(Funcs (Y,Z)) is Function-yielding
thus the Function of X,(Funcs (Y,Z)) is Function-yielding ; :: thesis: verum