for X, Y, Z being set holds Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z))