--- a/src/ZF/ZF.thy Wed May 08 10:14:35 2002 +0200
+++ b/src/ZF/ZF.thy Wed May 08 10:15:04 2002 +0200
@@ -71,7 +71,8 @@
range :: i => i
field :: i => i
converse :: i => i
- function :: i => o (*is a relation a function?*)
+ relation :: i => o (*recognizes sets of pairs*)
+ function :: i => o (*recognizes functions; can have non-pairs*)
Lambda :: [i, i => i] => i
restrict :: [i, i] => i
@@ -251,8 +252,9 @@
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"
range_def "range(r) == domain(converse(r))"
field_def "field(r) == domain(r) Un range(r)"
- function_def "function(r) == ALL x y. <x,y>:r -->
- (ALL y'. <x,y'>:r --> y=y')"
+ relation_def "relation(r) == ALL z:r. EX x y. z = <x,y>"
+ function_def "function(r) ==
+ ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')"
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
vimage_def "r -`` A == converse(r)``A"