Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | fofun | |- ( F : A -onto-> B -> Fun F ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof | |- ( F : A -onto-> B -> F : A --> B ) |
|
2 | 1 | ffund | |- ( F : A -onto-> B -> Fun F ) |