:: deftheorem Def1 defines bool MBOOLEAN:def 1 :
Lm1:
for i, I, X being set
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
Lm2:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
Lm3:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
Lm4:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
Lm5:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
theorem Th1: :: MBOOLEAN:1
theorem :: MBOOLEAN:2
theorem :: MBOOLEAN:3
theorem :: MBOOLEAN:4
theorem :: MBOOLEAN:5
theorem :: MBOOLEAN:6
theorem :: MBOOLEAN:7
theorem :: MBOOLEAN:8
theorem :: MBOOLEAN:9
theorem :: MBOOLEAN:10
theorem :: MBOOLEAN:11
theorem :: MBOOLEAN:12
theorem :: MBOOLEAN:13
theorem :: MBOOLEAN:14
canceled;
theorem :: MBOOLEAN:15
theorem :: MBOOLEAN:16
theorem :: MBOOLEAN:17
theorem :: MBOOLEAN:18
theorem :: MBOOLEAN:19
theorem :: MBOOLEAN:20
:: deftheorem Def2 defines union MBOOLEAN:def 2 :
Lm6:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
Lm7:
for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
theorem :: MBOOLEAN:21
theorem :: MBOOLEAN:22
theorem :: MBOOLEAN:23
theorem :: MBOOLEAN:24
theorem :: MBOOLEAN:25
theorem :: MBOOLEAN:26
theorem :: MBOOLEAN:27
theorem :: MBOOLEAN:28
theorem :: MBOOLEAN:29
theorem :: MBOOLEAN:30
theorem :: MBOOLEAN:31
theorem :: MBOOLEAN:32
theorem :: MBOOLEAN:33
theorem :: MBOOLEAN:34
theorem :: MBOOLEAN:35
theorem :: MBOOLEAN:36
theorem :: MBOOLEAN:37