:: COMSEQ_1 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: COMSEQ_1:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: COMSEQ_1:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def1 defines non-zero COMSEQ_1:def 1 :
theorem Th3: :: COMSEQ_1:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: COMSEQ_1:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th6: :: COMSEQ_1:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let C be non
empty set ;
let f1,
f2 be
PartFunc of
C,
COMPLEX ;
deffunc H1(
set )
-> Element of
COMPLEX =
(f1 /. $1) + (f2 /. $1);
defpred S1[
set ]
means $1
in (dom f1) /\ (dom f2);
set X =
(dom f1) /\ (dom f2);
func f1 + f2 -> PartFunc of
C,
COMPLEX means :
Def2:
:: COMSEQ_1:def 2
(
dom it = (dom f1) /\ (dom f2) & ( for
c being
Element of
C st
c in dom it holds
it . c = (f1 /. c) + (f2 /. c) ) );
existence
ex b1 being PartFunc of C, COMPLEX st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) + (f2 /. c) ) )
uniqueness
for b1, b2 being PartFunc of C, COMPLEX st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) + (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 /. c) + (f2 /. c) ) holds
b1 = b2
commutativity
for b1, f1, f2 being PartFunc of C, COMPLEX st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) + (f2 /. c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 /. c) + (f1 /. c) ) )
;
deffunc H2(
set )
-> Element of
COMPLEX =
(f1 /. $1) * (f2 /. $1);
func f1 (#) f2 -> PartFunc of
C,
COMPLEX means :
Def3:
:: COMSEQ_1:def 3
(
dom it = (dom f1) /\ (dom f2) & ( for
c being
Element of
C st
c in dom it holds
it . c = (f1 /. c) * (f2 /. c) ) );
existence
ex b1 being PartFunc of C, COMPLEX st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) * (f2 /. c) ) )
uniqueness
for b1, b2 being PartFunc of C, COMPLEX st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) * (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 /. c) * (f2 /. c) ) holds
b1 = b2
commutativity
for b1, f1, f2 being PartFunc of C, COMPLEX st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 /. c) * (f2 /. c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 /. c) * (f1 /. c) ) )
;
end;
:: deftheorem Def2 defines + COMSEQ_1:def 2 :
:: deftheorem Def3 defines (#) COMSEQ_1:def 3 :
:: deftheorem Def4 defines + COMSEQ_1:def 4 :
:: deftheorem Def5 defines (#) COMSEQ_1:def 5 :
:: deftheorem Def6 defines (#) COMSEQ_1:def 6 :
:: deftheorem Def7 defines (#) COMSEQ_1:def 7 :
:: deftheorem Def8 defines - COMSEQ_1:def 8 :
:: deftheorem Def9 defines - COMSEQ_1:def 9 :
:: deftheorem defines - COMSEQ_1:def 10 :
:: deftheorem Def11 defines " COMSEQ_1:def 11 :
:: deftheorem defines /" COMSEQ_1:def 12 :
:: deftheorem Def13 defines |. COMSEQ_1:def 13 :
:: deftheorem Def14 defines |. COMSEQ_1:def 14 :
theorem :: COMSEQ_1:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th9: :: COMSEQ_1:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th11: :: COMSEQ_1:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: COMSEQ_1:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: COMSEQ_1:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: COMSEQ_1:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: COMSEQ_1:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: COMSEQ_1:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: COMSEQ_1:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: COMSEQ_1:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: COMSEQ_1:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: COMSEQ_1:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: COMSEQ_1:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: COMSEQ_1:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th26: :: COMSEQ_1:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th30: :: COMSEQ_1:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: COMSEQ_1:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: COMSEQ_1:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th33: :: COMSEQ_1:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: COMSEQ_1:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th38: :: COMSEQ_1:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th40: :: COMSEQ_1:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th41: :: COMSEQ_1:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th43: :: COMSEQ_1:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th44: :: COMSEQ_1:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th46: :: COMSEQ_1:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th49: :: COMSEQ_1:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th51: :: COMSEQ_1:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: COMSEQ_1:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) 