:: Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received May 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
(- 1) " = - 1
;
:: deftheorem RFUNCT_1:def 1 :
canceled;
:: deftheorem RFUNCT_1:def 2 :
canceled;
:: deftheorem RFUNCT_1:def 3 :
canceled;
:: deftheorem Def4 defines / RFUNCT_1:def 4 :
:: deftheorem RFUNCT_1:def 5 :
canceled;
:: deftheorem RFUNCT_1:def 6 :
canceled;
:: deftheorem RFUNCT_1:def 7 :
canceled;
:: deftheorem Def8 defines ^ RFUNCT_1:def 8 :
theorem :: RFUNCT_1:1
canceled;
theorem :: RFUNCT_1:2
canceled;
theorem :: RFUNCT_1:3
canceled;
theorem :: RFUNCT_1:4
canceled;
theorem :: RFUNCT_1:5
canceled;
theorem :: RFUNCT_1:6
canceled;
theorem :: RFUNCT_1:7
canceled;
theorem :: RFUNCT_1:8
canceled;
theorem :: RFUNCT_1:9
canceled;
theorem :: RFUNCT_1:10
canceled;
theorem Th11: :: RFUNCT_1:11
theorem Th12: :: RFUNCT_1:12
theorem Th13: :: RFUNCT_1:13
theorem Th14: :: RFUNCT_1:14
theorem Th15: :: RFUNCT_1:15
theorem Th16: :: RFUNCT_1:16
theorem Th17: :: RFUNCT_1:17
theorem :: RFUNCT_1:18
canceled;
theorem :: RFUNCT_1:19
theorem :: RFUNCT_1:20
canceled;
theorem Th21: :: RFUNCT_1:21
theorem Th22: :: RFUNCT_1:22
theorem :: RFUNCT_1:23
theorem Th24: :: RFUNCT_1:24
theorem Th25: :: RFUNCT_1:25
theorem Th26: :: RFUNCT_1:26
theorem :: RFUNCT_1:27
theorem :: RFUNCT_1:28
theorem :: RFUNCT_1:29
theorem :: RFUNCT_1:30
theorem :: RFUNCT_1:31
theorem :: RFUNCT_1:32
theorem :: RFUNCT_1:33
theorem :: RFUNCT_1:34
theorem :: RFUNCT_1:35
theorem Th36: :: RFUNCT_1:36
theorem :: RFUNCT_1:37
theorem :: RFUNCT_1:38
canceled;
theorem :: RFUNCT_1:39
canceled;
theorem :: RFUNCT_1:40
canceled;
theorem :: RFUNCT_1:41
canceled;
theorem Th42: :: RFUNCT_1:42
theorem Th43: :: RFUNCT_1:43
theorem Th44: :: RFUNCT_1:44
theorem :: RFUNCT_1:45
theorem Th46: :: RFUNCT_1:46
theorem Th47: :: RFUNCT_1:47
theorem Th48: :: RFUNCT_1:48
theorem :: RFUNCT_1:49
theorem Th50: :: RFUNCT_1:50
theorem Th51: :: RFUNCT_1:51
theorem Th52: :: RFUNCT_1:52
theorem :: RFUNCT_1:53
theorem :: RFUNCT_1:54
theorem :: RFUNCT_1:55
theorem Th56: :: RFUNCT_1:56
theorem :: RFUNCT_1:57
theorem :: RFUNCT_1:58
theorem :: RFUNCT_1:59
theorem Th60: :: RFUNCT_1:60
theorem Th61: :: RFUNCT_1:61
theorem Th62: :: RFUNCT_1:62
theorem :: RFUNCT_1:63
theorem :: RFUNCT_1:64
theorem Th65: :: RFUNCT_1:65
theorem Th66: :: RFUNCT_1:66
theorem Th67: :: RFUNCT_1:67
theorem :: RFUNCT_1:68
theorem :: RFUNCT_1:69
theorem Th70: :: RFUNCT_1:70
theorem Th71: :: RFUNCT_1:71
theorem :: RFUNCT_1:72
theorem :: RFUNCT_1:73
theorem :: RFUNCT_1:74
theorem :: RFUNCT_1:75
theorem :: RFUNCT_1:76
theorem Th77: :: RFUNCT_1:77
theorem :: RFUNCT_1:78
theorem :: RFUNCT_1:79
theorem :: RFUNCT_1:80
theorem :: RFUNCT_1:81
theorem :: RFUNCT_1:82
canceled;
theorem :: RFUNCT_1:83
theorem Th84: :: RFUNCT_1:84
theorem :: RFUNCT_1:85
theorem :: RFUNCT_1:86
theorem Def9: :: RFUNCT_1:87
theorem Def10: :: RFUNCT_1:88
theorem Th89: :: RFUNCT_1:89
theorem :: RFUNCT_1:90
theorem :: RFUNCT_1:91
theorem :: RFUNCT_1:92
theorem :: RFUNCT_1:93
theorem :: RFUNCT_1:94
theorem Th95: :: RFUNCT_1:95
theorem Th96: :: RFUNCT_1:96
theorem Th97: :: RFUNCT_1:97
theorem :: RFUNCT_1:98
theorem Th99: :: RFUNCT_1:99
theorem Th100: :: RFUNCT_1:100
theorem Th101: :: RFUNCT_1:101
theorem Th102: :: RFUNCT_1:102
theorem Th103: :: RFUNCT_1:103
theorem :: RFUNCT_1:104
theorem :: RFUNCT_1:105
theorem Th106: :: RFUNCT_1:106
theorem Th107: :: RFUNCT_1:107
theorem Th108: :: RFUNCT_1:108
theorem :: RFUNCT_1:109
theorem :: RFUNCT_1:110
theorem :: RFUNCT_1:111