environ
vocabularies HIDDEN, PBOOLE, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, FUNCOP_1, TARSKI, FUNCT_2, FINSET_1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE;
definitions PBOOLE;
theorems CARD_2, SETFAM_1, FUNCOP_1, FRAENKEL, FUNCT_4, PBOOLE, FINSET_1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, RELAT_1, FUNCT_1;
schemes PBOOLE;
registrations XBOOLE_0, SUBSET_1, FUNCOP_1, PRE_CIRC;
constructors HIDDEN, FUNCT_4, PBOOLE, FINSET_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCOP_1;
expansions PBOOLE;
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))
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))