thus f quotient (E,F) is Function of (Class E),(Class F) ; :: thesis: verum