f " is PartFunc of C,REAL ;
hence Inv f is PartFunc of C,REAL ; :: thesis: verum