B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f 
g) 
f g(x) = if x dom(f)
f(x) else g(x) fi B(x)B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f g) 
x dom(f) 
x dom(g)| Rank | Theorem | Name |
| 4 | B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x dom(f g) f g(x) = if x dom(f) f(x) else g(x) fi B(x) | [fpf-join-ap] |
| cites the following: | ||
| 3 | B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x dom(f g) x dom(f) x dom(g) | [fpf-join-dom] |