eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x 
dom(f) 
x dom(f)B:(A
Type), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A.
Thm* x
dom(f) = x dom(f) 
| Rank | Theorem | Name |
| 4 | eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x dom(f) x dom(f) | [fpf-dom_functionality2] |
| cites the following: | ||
| 3 | B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A.
Thm* x dom(f) = x dom(f) | [fpf-dom_functionality] |