On Partial functions (Solution)

The answer is NO !!!! .
The axiom pfun_extensionality allows you to prove 0=1 (look at this file ).
If you remove this axiom, the formalization is OK.
Going home