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