:: Arithmetic Operations on Functions from Sets into Functional Sets
:: by Artur Korni{\l}owicz
::
:: Received October 15, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem defines DOMS VALUED_2:def 1 :
:: deftheorem Def1 defines complex-functions-membered VALUED_2:def 2 :
:: deftheorem Def2 defines ext-real-functions-membered VALUED_2:def 3 :
:: deftheorem Def3 defines real-functions-membered VALUED_2:def 4 :
:: deftheorem Def4 defines rational-functions-membered VALUED_2:def 5 :
:: deftheorem Def5 defines integer-functions-membered VALUED_2:def 6 :
:: deftheorem Def6 defines natural-functions-membered VALUED_2:def 7 :
consider ff being natural-valued Function;
:: deftheorem Def7 defines C_PFuncs VALUED_2:def 8 :
:: deftheorem Def8 defines C_Funcs VALUED_2:def 9 :
:: deftheorem Def9 defines E_PFuncs VALUED_2:def 10 :
:: deftheorem Def10 defines E_Funcs VALUED_2:def 11 :
:: deftheorem Def11 defines R_PFuncs VALUED_2:def 12 :
:: deftheorem Def12 defines R_Funcs VALUED_2:def 13 :
:: deftheorem Def13 defines Q_PFuncs VALUED_2:def 14 :
:: deftheorem Def14 defines Q_Funcs VALUED_2:def 15 :
:: deftheorem Def15 defines I_PFuncs VALUED_2:def 16 :
:: deftheorem Def16 defines I_Funcs VALUED_2:def 17 :
:: deftheorem Def17 defines N_PFuncs VALUED_2:def 18 :
:: deftheorem Def18 defines N_Funcs VALUED_2:def 19 :
theorem Th2: :: VALUED_2:1
theorem Th3: :: VALUED_2:2
theorem Th4: :: VALUED_2:3
theorem Th5: :: VALUED_2:4
theorem Th6: :: VALUED_2:5
theorem Th7: :: VALUED_2:6
:: deftheorem Def19 defines complex-functions-valued VALUED_2:def 20 :
:: deftheorem Def20 defines ext-real-functions-valued VALUED_2:def 21 :
:: deftheorem Def21 defines real-functions-valued VALUED_2:def 22 :
:: deftheorem Def22 defines rational-functions-valued VALUED_2:def 23 :
:: deftheorem Def23 defines integer-functions-valued VALUED_2:def 24 :
:: deftheorem Def24 defines natural-functions-valued VALUED_2:def 25 :
:: deftheorem defines complex-functions-valued VALUED_2:def 26 :
:: deftheorem defines ext-real-functions-valued VALUED_2:def 27 :
:: deftheorem defines real-functions-valued VALUED_2:def 28 :
:: deftheorem defines rational-functions-valued VALUED_2:def 29 :
:: deftheorem defines integer-functions-valued VALUED_2:def 30 :
:: deftheorem defines natural-functions-valued VALUED_2:def 31 :
theorem Tha: :: VALUED_2:7
theorem Thb: :: VALUED_2:8
theorem Thc: :: VALUED_2:9
theorem Th81: :: VALUED_2:10
theorem Th82: :: VALUED_2:11
theorem Th8: :: VALUED_2:12
theorem Th9: :: VALUED_2:13
theorem Th10: :: VALUED_2:14
theorem Th11: :: VALUED_2:15
theorem Th12: :: VALUED_2:16
theorem Th13a: :: VALUED_2:17
theorem Th13: :: VALUED_2:18
theorem Th14b: :: VALUED_2:19
theorem Th14a: :: VALUED_2:20
theorem Th14: :: VALUED_2:21
theorem Th17: :: VALUED_2:22
theorem Th18: :: VALUED_2:23
theorem Th19: :: VALUED_2:24
theorem Th13b: :: VALUED_2:25
theorem :: VALUED_2:26
theorem Th13d: :: VALUED_2:27
:: deftheorem defines (/) VALUED_2:def 32 :
theorem :: VALUED_2:28
theorem :: VALUED_2:29
theorem Th20: :: VALUED_2:30
theorem Th21: :: VALUED_2:31
theorem :: VALUED_2:32
theorem Thd: :: VALUED_2:33
theorem :: VALUED_2:34
theorem :: VALUED_2:35
theorem :: VALUED_2:36
theorem :: VALUED_2:37
theorem :: VALUED_2:38
theorem :: VALUED_2:39
theorem :: VALUED_2:40
:: deftheorem Def32 defines <-> VALUED_2:def 33 :
theorem :: VALUED_2:41
theorem :: VALUED_2:42
:: deftheorem defines (-) VALUED_2:def 34 :
:: deftheorem Def34 defines </> VALUED_2:def 35 :
theorem :: VALUED_2:43
:: deftheorem Def35 defines abs VALUED_2:def 36 :
theorem :: VALUED_2:44
:: deftheorem Def36 defines [+] VALUED_2:def 37 :
theorem :: VALUED_2:45
theorem :: VALUED_2:46
:: deftheorem defines [-] VALUED_2:def 38 :
theorem :: VALUED_2:47
theorem :: VALUED_2:48
theorem :: VALUED_2:49
theorem :: VALUED_2:50
theorem :: VALUED_2:51
theorem :: VALUED_2:52
:: deftheorem Def38 defines [#] VALUED_2:def 39 :
theorem :: VALUED_2:53
theorem :: VALUED_2:54
:: deftheorem defines [/] VALUED_2:def 40 :
theorem :: VALUED_2:55
theorem :: VALUED_2:56
theorem :: VALUED_2:57
theorem :: VALUED_2:58
:: deftheorem Def40 defines <+> VALUED_2:def 41 :
theorem :: VALUED_2:59
theorem :: VALUED_2:60
:: deftheorem defines <-> VALUED_2:def 42 :
theorem Th35: :: VALUED_2:61
theorem Th36: :: VALUED_2:62
theorem :: VALUED_2:63
theorem :: VALUED_2:64
theorem :: VALUED_2:65
theorem :: VALUED_2:66
theorem :: VALUED_2:67
:: deftheorem Def42 defines <#> VALUED_2:def 43 :
theorem :: VALUED_2:68
theorem :: VALUED_2:69
theorem :: VALUED_2:70
:: deftheorem defines </> VALUED_2:def 44 :
theorem Th100: :: VALUED_2:71
theorem Th101: :: VALUED_2:72
theorem :: VALUED_2:73
:: deftheorem Def44 defines <++> VALUED_2:def 45 :
theorem Th43: :: VALUED_2:74
theorem :: VALUED_2:75
theorem :: VALUED_2:76
:: deftheorem Def45 defines <--> VALUED_2:def 46 :
theorem :: VALUED_2:77
theorem :: VALUED_2:78
theorem :: VALUED_2:79
theorem :: VALUED_2:80
theorem :: VALUED_2:81
theorem :: VALUED_2:82
:: deftheorem Def46 defines <##> VALUED_2:def 47 :
theorem Th49: :: VALUED_2:83
theorem :: VALUED_2:84
theorem :: VALUED_2:85
theorem :: VALUED_2:86
theorem Th51: :: VALUED_2:87
theorem :: VALUED_2:88
theorem Th53: :: VALUED_2:89
theorem :: VALUED_2:90
:: deftheorem Def47 defines <//> VALUED_2:def 48 :
theorem :: VALUED_2:91
theorem :: VALUED_2:92
theorem :: VALUED_2:93
theorem :: VALUED_2:94
theorem :: VALUED_2:95
theorem :: VALUED_2:96
theorem :: VALUED_2:97