:: FINSEQOP semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: FINSEQOP:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th4: :: FINSEQOP:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: FINSEQOP:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: FINSEQOP:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: FINSEQOP:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm1:
for C, D being non empty set
for f being Function of C,D
for T being Element of 0 -tuples_on C holds f * T = <*> D
Lm2:
for D', D, E being non empty set
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D'
for T being Element of 0 -tuples_on D holds F .: T,T' = <*> E
Lm3:
for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for T' being Element of 0 -tuples_on D' holds F [;] d,T' = <*> E
Lm4:
for D', D, E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for T being Element of 0 -tuples_on D holds F [:] T,d' = <*> E
theorem Th11: :: FINSEQOP:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th13: :: FINSEQOP:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: FINSEQOP:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th18: :: FINSEQOP:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm5:
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D holds T is Function of Seg i,D
theorem Th25: :: FINSEQOP:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th26: :: FINSEQOP:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th36: :: FINSEQOP:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th37: :: FINSEQOP:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th38: :: FINSEQOP:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
C,
E,
D being non
empty set for
f,
f' being
Function of
C,
D for
h being
Function of
D,
E for
F being
BinOp of
D for
H being
BinOp of
E st ( for
d1,
d2 being
Element of
D holds
h . (F . d1,d2) = H . (h . d1),
(h . d2) ) holds
h * (F .: f,f') = H .: (h * f),
(h * f')
theorem Th39: :: FINSEQOP:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th40: :: FINSEQOP:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:42 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th44: :: FINSEQOP:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th45: :: FINSEQOP:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th46: :: FINSEQOP:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:47 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:48 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th49: :: FINSEQOP:49 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th50: :: FINSEQOP:50 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th51: :: FINSEQOP:51 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:52 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:53 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:54 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:55 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:56 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:57 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:58 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:59 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def1 defines is_an_inverseOp_wrt FINSEQOP:def 1 :
:: deftheorem Def2 defines having_an_inverseOp FINSEQOP:def 2 :
:: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def 3 :
theorem :: FINSEQOP:60 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: FINSEQOP:61 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: FINSEQOP:62 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th63: :: FINSEQOP:63 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th64: :: FINSEQOP:64 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th65: :: FINSEQOP:65 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th66: :: FINSEQOP:66 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th67: :: FINSEQOP:67 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th68: :: FINSEQOP:68 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th69: :: FINSEQOP:69 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th70: :: FINSEQOP:70 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th71: :: FINSEQOP:71 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:72 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:73 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:74 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th75: :: FINSEQOP:75 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th76: :: FINSEQOP:76 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:77 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:78 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th79: :: FINSEQOP:79 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:80 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines * FINSEQOP:def 4 :
theorem :: FINSEQOP:81 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th82: :: FINSEQOP:82 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th83: :: FINSEQOP:83 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th84: :: FINSEQOP:84 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
D,
D',
E,
C,
C' being non
empty set for
F being
Function of
[:D,D':],
E for
f being
Function of
C,
D for
g being
Function of
C',
D' holds
F * f,
g is
Function of
[:C,C':],
E
theorem :: FINSEQOP:85 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th86: :: FINSEQOP:86 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
D,
D',
E,
C,
C' being non
empty set for
c being
Element of
C for
c' being
Element of
C' for
F being
Function of
[:D,D':],
E for
f being
Function of
C,
D for
g being
Function of
C',
D' holds
(F * f,g) . c,
c' = F . (f . c),
(g . c')
theorem Th87: :: FINSEQOP:87 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th88: :: FINSEQOP:88 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:89 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:90 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:91 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:92 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:93 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FINSEQOP:94 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
D being non
empty set for
F,
G being
BinOp of
D st
F is
commutative &
F is
associative &
F has_a_unity &
F has_an_inverseOp &
G = F * (id D),
(the_inverseOp_wrt F) holds
for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (G . d1,d2),
(G . d3,d4) = G . (F . d1,d3),
(F . d2,d4)