thus ~ f is Function of [:D,C:],E ; :: thesis: verum