PBOOLE: Manysorted Sets

:: Manysorted Sets
:: by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993 Association of Mizar Users

begin

theorem :: PBOOLE:1

for f being Function st f is non-empty holds
rng f is with_non-empty_elements ;

theorem :: PBOOLE:2

for f being Function holds
( f is empty-yielding iff ( f = {} or rng f = {{}} ) )

proof end;

registration

let I be set ;
cluster Relation-like I -defined Function-like total set ;
existence

proof end;

end;

definition

let I be set ;
canceled;
canceled;
canceled;
mode ManySortedSet of I is I -defined total Function;

end;

:: deftheorem PBOOLE:def 1 :

:: deftheorem PBOOLE:def 2 :

:: deftheorem PBOOLE:def 3 :

scheme :: PBOOLE:sch 1
KuratowskiFunction{ F₁() -> set , F₂( set ) -> set } :

ex f being ManySortedSet of F₁() st
for e being set st e in F₁() holds
f . e in F₂(e)

provided

A1: for e being set st e in F₁() holds
F₂(e) <> {}

proof end;

definition

let I be set ;
let X, Y be ManySortedSet of I;
pred X in Y means :Def4: :: PBOOLE:def 4
for i being set st i in I holds
X . i in Y . i;
pred X c= Y means :Def5: :: PBOOLE:def 5
for i being set st i in I holds
X . i c= Y . i;
reflexivity ;

end;

:: deftheorem Def4 defines in PBOOLE:def 4 :

:: deftheorem Def5 defines c= PBOOLE:def 5 :

definition

let I be non empty set ;
let X, Y be ManySortedSet of I;
:: original: in
redefine pred X in Y;
asymmetry

proof end;

end;

scheme :: PBOOLE:sch 2
PSeparation{ F₁() -> set , F₂() -> ManySortedSet of F₁(), P₁[ set , set ] } :

ex X being ManySortedSet of F₁() st
for i being set st i in F₁() holds
for e being set holds
( e in X . i iff ( e in F₂() . i & P₁[i,e] ) )

proof end;

theorem Th3: :: PBOOLE:3

for I being set
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i = Y . i ) holds
X = Y

proof end;

definition

let I be set ;
func [[0]] I -> ManySortedSet of I equals :: PBOOLE:def 6
I --> {};
coherence ;
correctness ;
let X, Y be ManySortedSet of I;
func X \/ Y -> ManySortedSet of I means :Def7: :: PBOOLE:def 7
for i being set st i in I holds
it . i = (X . i) \/ (Y . i);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func X /\ Y -> ManySortedSet of I means :Def8: :: PBOOLE:def 8
for i being set st i in I holds
it . i = (X . i) /\ (Y . i);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func X \ Y -> ManySortedSet of I means :Def9: :: PBOOLE:def 9
for i being set st i in I holds
it . i = (X . i) \ (Y . i);
existence

proof end;

uniqueness

proof end;

pred X overlaps Y means :Def10: :: PBOOLE:def 10
for i being set st i in I holds
X . i meets Y . i;
symmetry ;
pred X misses Y means :Def11: :: PBOOLE:def 11
for i being set st i in I holds
X . i misses Y . i;
symmetry ;

end;

:: deftheorem defines [[0]] PBOOLE:def 6 :

:: deftheorem Def7 defines \/ PBOOLE:def 7 :

:: deftheorem Def8 defines /\ PBOOLE:def 8 :

:: deftheorem Def9 defines \ PBOOLE:def 9 :

:: deftheorem Def10 defines overlaps PBOOLE:def 10 :

:: deftheorem Def11 defines misses PBOOLE:def 11 :

notation

let I be set ;
let X, Y be ManySortedSet of I;
antonym X meets Y for X misses Y;

end;

definition

let I be set ;
let X, Y be ManySortedSet of I;
func X \+\ Y -> ManySortedSet of I equals :: PBOOLE:def 12
(X \ Y) \/ (Y \ X);
correctness ;
commutativity ;

end;

:: deftheorem defines \+\ PBOOLE:def 12 :

theorem Th4: :: PBOOLE:4

for I being set
for X, Y being ManySortedSet of I
for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)

proof end;

theorem Th5: :: PBOOLE:5

for i, I being set holds ([[0]] I) . i = {}

proof end;

theorem Th6: :: PBOOLE:6

for I being set
for X being ManySortedSet of I st ( for i being set st i in I holds
X . i = {} ) holds
X = [[0]] I

proof end;

theorem Th7: :: PBOOLE:7

for I being set
for x, X, Y being ManySortedSet of I st ( x in X or x in Y ) holds
x in X \/ Y

proof end;

theorem Th8: :: PBOOLE:8

for I being set
for x, X, Y being ManySortedSet of I holds
( x in X /\ Y iff ( x in X & x in Y ) )

proof end;

theorem Th9: :: PBOOLE:9

for I being set
for x, X, Y being ManySortedSet of I st x in X & X c= Y holds
x in Y

proof end;

theorem Th10: :: PBOOLE:10

for I being set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlaps Y

proof end;

theorem Th11: :: PBOOLE:11

for I being set
for X, Y being ManySortedSet of I st X overlaps Y holds
ex x being ManySortedSet of I st
( x in X & x in Y )

proof end;

theorem :: PBOOLE:12

for I being set
for x, X, Y being ManySortedSet of I st x in X \ Y holds
x in X

proof end;

begin

definition

let I be set ;
let X, Y be ManySortedSet of I;
:: original: =
redefine pred X = Y means :Def13: :: PBOOLE:def 13
( X c= Y & Y c= X );
compatibility

proof end;

end;

:: deftheorem Def13 defines = PBOOLE:def 13 :

theorem :: PBOOLE:13

canceled;

theorem :: PBOOLE:14

canceled;

theorem Th15: :: PBOOLE:15

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y c= Z holds
X c= Z

proof end;

theorem Th16: :: PBOOLE:16

for I being set
for X, Y being ManySortedSet of I holds
( X c= X \/ Y & Y c= X \/ Y )

proof end;

theorem Th17: :: PBOOLE:17

for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y c= X & X /\ Y c= Y )

proof end;

theorem Th18: :: PBOOLE:18

for I being set
for X, Z, Y being ManySortedSet of I st X c= Z & Y c= Z holds
X \/ Y c= Z

proof end;

theorem Th19: :: PBOOLE:19

for I being set
for Z, X, Y being ManySortedSet of I st Z c= X & Z c= Y holds
Z c= X /\ Y

proof end;

theorem :: PBOOLE:20

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
( X \/ Z c= Y \/ Z & Z \/ X c= Z \/ Y )

proof end;

theorem Th21: :: PBOOLE:21

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
( X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y )

proof end;

theorem Th22: :: PBOOLE:22

for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \/ Z c= Y \/ V

proof end;

theorem :: PBOOLE:23

for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X /\ Z c= Y /\ V

proof end;

theorem Th24: :: PBOOLE:24

for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( X \/ Y = Y & Y \/ X = Y )

proof end;

theorem Th25: :: PBOOLE:25

for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( X /\ Y = X & Y /\ X = X )

proof end;

theorem :: PBOOLE:26

for I being set
for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z

proof end;

theorem :: PBOOLE:27

for I being set
for X, Z, Y being ManySortedSet of I st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z

proof end;

theorem :: PBOOLE:28

for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y \/ Z iff ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) )

proof end;

theorem :: PBOOLE:29

for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y /\ Z iff ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) )

proof end;

theorem :: PBOOLE:30

canceled;

theorem :: PBOOLE:31

canceled;

theorem :: PBOOLE:32

canceled;

theorem :: PBOOLE:33

canceled;

theorem Th34: :: PBOOLE:34

for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = X \/ (Y \/ Z)

proof end;

theorem Th35: :: PBOOLE:35

for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = X /\ (Y /\ Z)

proof end;

theorem Th36: :: PBOOLE:36

for I being set
for X, Y being ManySortedSet of I holds
( X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )

proof end;

theorem Th37: :: PBOOLE:37

for I being set
for X, Y being ManySortedSet of I holds
( X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )

proof end;

theorem Th38: :: PBOOLE:38

for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)

proof end;

theorem Th39: :: PBOOLE:39

for I being set
for X, Y, Z being ManySortedSet of I holds
( X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z) & (Y /\ Z) \/ X = (Y \/ X) /\ (Z \/ X) )

proof end;

theorem :: PBOOLE:40

for I being set
for X, Y, Z being ManySortedSet of I st (X /\ Y) \/ (X /\ Z) = X holds
X c= Y \/ Z

proof end;

theorem :: PBOOLE:41

for I being set
for X, Y, Z being ManySortedSet of I st (X \/ Y) /\ (X \/ Z) = X holds
Y /\ Z c= X

proof end;

theorem :: PBOOLE:42

for I being set
for X, Y, Z being ManySortedSet of I holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)

proof end;

theorem :: PBOOLE:43

for I being set
for X, Y, Z being ManySortedSet of I st X \/ Y c= Z holds
( X c= Z & Y c= Z )

proof end;

theorem :: PBOOLE:44

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y /\ Z holds
( X c= Y & X c= Z )

proof end;

theorem :: PBOOLE:45

for I being set
for X, Y, Z being ManySortedSet of I holds
( (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) & X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z) )

proof end;

theorem :: PBOOLE:46

for I being set
for X, Y, Z being ManySortedSet of I holds
( (X /\ Y) /\ Z = (X /\ Z) /\ (Y /\ Z) & X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z) )

proof end;

theorem :: PBOOLE:47

for I being set
for X, Y being ManySortedSet of I holds
( X \/ (X \/ Y) = X \/ Y & (X \/ Y) \/ Y = X \/ Y )

proof end;

theorem :: PBOOLE:48

for I being set
for X, Y being ManySortedSet of I holds
( X /\ (X /\ Y) = X /\ Y & (X /\ Y) /\ Y = X /\ Y )

proof end;

begin

theorem Th49: :: PBOOLE:49

for I being set
for X being ManySortedSet of I holds [[0]] I c= X

proof end;

theorem Th50: :: PBOOLE:50

for I being set
for X being ManySortedSet of I st X c= [[0]] I holds
X = [[0]] I

proof end;

theorem :: PBOOLE:51

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y /\ Z = [[0]] I holds
X = [[0]] I by Th19, Th50;

theorem :: PBOOLE:52

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y /\ Z = [[0]] I holds
X /\ Z = [[0]] I

proof end;

theorem Th53: :: PBOOLE:53

for I being set
for X being ManySortedSet of I holds
( X \/ ([[0]] I) = X & ([[0]] I) \/ X = X )

proof end;

theorem :: PBOOLE:54

for I being set
for X, Y being ManySortedSet of I st X \/ Y = [[0]] I holds
( X = [[0]] I & Y = [[0]] I )

proof end;

theorem :: PBOOLE:55

for I being set
for X being ManySortedSet of I holds
( X /\ ([[0]] I) = [[0]] I & ([[0]] I) /\ X = [[0]] I )

proof end;

theorem :: PBOOLE:56

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y \/ Z & X /\ Z = [[0]] I holds
X c= Y

proof end;

theorem :: PBOOLE:57

for I being set
for Y, X being ManySortedSet of I st Y c= X & X /\ Y = [[0]] I holds
Y = [[0]] I by Th25;

begin

theorem Th58: :: PBOOLE:58

for I being set
for X, Y being ManySortedSet of I holds
( X \ Y = [[0]] I iff X c= Y )

proof end;

theorem Th59: :: PBOOLE:59

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
X \ Z c= Y \ Z

proof end;

theorem Th60: :: PBOOLE:60

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
Z \ Y c= Z \ X

proof end;

theorem :: PBOOLE:61

for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \ V c= Y \ Z

proof end;

theorem Th62: :: PBOOLE:62

for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X

proof end;

theorem :: PBOOLE:63

for I being set
for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [[0]] I

proof end;

theorem :: PBOOLE:64

for I being set
for X being ManySortedSet of I holds X \ X = [[0]] I by Th58;

theorem Th65: :: PBOOLE:65

for I being set
for X being ManySortedSet of I holds X \ ([[0]] I) = X

proof end;

theorem Th66: :: PBOOLE:66

for I being set
for X being ManySortedSet of I holds ([[0]] I) \ X = [[0]] I

proof end;

theorem :: PBOOLE:67

for I being set
for X, Y being ManySortedSet of I holds
( X \ (X \/ Y) = [[0]] I & X \ (Y \/ X) = [[0]] I )

proof end;

theorem Th68: :: PBOOLE:68

for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ Z

proof end;

theorem Th69: :: PBOOLE:69

for I being set
for X, Y being ManySortedSet of I holds
( (X \ Y) /\ Y = [[0]] I & Y /\ (X \ Y) = [[0]] I )

proof end;

theorem Th70: :: PBOOLE:70

for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)

proof end;

theorem Th71: :: PBOOLE:71

for I being set
for X, Y being ManySortedSet of I holds
( (X \ Y) \/ (X /\ Y) = X & (X /\ Y) \/ (X \ Y) = X )

proof end;

theorem :: PBOOLE:72

for I being set
for X, Y being ManySortedSet of I st X c= Y holds
( Y = X \/ (Y \ X) & Y = (Y \ X) \/ X )

proof end;

theorem Th73: :: PBOOLE:73

for I being set
for X, Y being ManySortedSet of I holds
( X \/ (Y \ X) = X \/ Y & (Y \ X) \/ X = Y \/ X )

proof end;

theorem Th74: :: PBOOLE:74

for I being set
for X, Y being ManySortedSet of I holds X \ (X \ Y) = X /\ Y

proof end;

theorem Th75: :: PBOOLE:75

for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)

proof end;

theorem Th76: :: PBOOLE:76

for I being set
for X, Y being ManySortedSet of I holds
( X \ (X /\ Y) = X \ Y & X \ (Y /\ X) = X \ Y )

proof end;

theorem :: PBOOLE:77

for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y = [[0]] I iff X \ Y = X )

proof end;

theorem Th78: :: PBOOLE:78

for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)

proof end;

theorem Th79: :: PBOOLE:79

for I being set
for X, Y, Z being ManySortedSet of I holds (X \ Y) \ Z = X \ (Y \/ Z)

proof end;

theorem :: PBOOLE:80

for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z)

proof end;

theorem Th81: :: PBOOLE:81

for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y

proof end;

theorem :: PBOOLE:82

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y \/ Z holds
( X \ Y c= Z & X \ Z c= Y )

proof end;

theorem Th83: :: PBOOLE:83

for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)

proof end;

theorem Th84: :: PBOOLE:84

for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y

proof end;

theorem :: PBOOLE:85

for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)

proof end;

theorem :: PBOOLE:86

for I being set
for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y

proof end;

theorem :: PBOOLE:87

for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)

proof end;

theorem :: PBOOLE:88

for I being set
for X, Y, Z being ManySortedSet of I st X \ Y c= Z holds
X c= Y \/ Z

proof end;

theorem :: PBOOLE:89

for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X \+\ Y by Th16;

theorem :: PBOOLE:90

canceled;

theorem :: PBOOLE:91

for I being set
for X being ManySortedSet of I holds
( X \+\ ([[0]] I) = X & ([[0]] I) \+\ X = X )

proof end;

theorem :: PBOOLE:92

for I being set
for X being ManySortedSet of I holds X \+\ X = [[0]] I by Th58;

theorem :: PBOOLE:93

canceled;

theorem :: PBOOLE:94

for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \/ (X /\ Y)

proof end;

theorem Th95: :: PBOOLE:95

for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \/ Y) \ (X /\ Y)

proof end;

theorem :: PBOOLE:96

for I being set
for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))

proof end;

theorem :: PBOOLE:97

for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)

proof end;

theorem Th98: :: PBOOLE:98

for I being set
for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)

proof end;

theorem :: PBOOLE:99

for I being set
for X, Y, Z being ManySortedSet of I st X \ Y c= Z & Y \ X c= Z holds
X \+\ Y c= Z by Th18;

theorem Th100: :: PBOOLE:100

for I being set
for X, Y being ManySortedSet of I holds X \/ Y = X \+\ (Y \ X)

proof end;

theorem Th101: :: PBOOLE:101

for I being set
for X, Y being ManySortedSet of I holds X /\ Y = X \+\ (X \ Y)

proof end;

theorem Th102: :: PBOOLE:102

for I being set
for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)

proof end;

theorem Th103: :: PBOOLE:103

for I being set
for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)

proof end;

theorem :: PBOOLE:104

for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)

proof end;

theorem :: PBOOLE:105

for I being set
for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)

proof end;

begin

theorem :: PBOOLE:106

for I being set
for X, Y, Z being ManySortedSet of I st ( X overlaps Y or X overlaps Z ) holds
X overlaps Y \/ Z

proof end;

theorem :: PBOOLE:107

canceled;

theorem Th108: :: PBOOLE:108

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y & Y c= Z holds
X overlaps Z

proof end;

theorem Th109: :: PBOOLE:109

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y & X c= Z holds
Z overlaps Y

proof end;

theorem Th110: :: PBOOLE:110

for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V & X overlaps Z holds
Y overlaps V

proof end;

theorem :: PBOOLE:111

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y /\ Z holds
( X overlaps Y & X overlaps Z )

proof end;

theorem :: PBOOLE:112

for I being set
for X, Z, V being ManySortedSet of I st X overlaps Z & X c= V holds
X overlaps Z /\ V

proof end;

theorem :: PBOOLE:113

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
X overlaps Y by Th62, Th108;

theorem :: PBOOLE:114

for I being set
for Y, Z, X being ManySortedSet of I st not Y overlaps Z holds
not X /\ Y overlaps X /\ Z

proof end;

theorem :: PBOOLE:115

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
Y overlaps X \ Z

proof end;

theorem Th116: :: PBOOLE:116

for I being set
for X, Y, Z being ManySortedSet of I st X meets Y & Y c= Z holds
X meets Z

proof end;

theorem :: PBOOLE:117

canceled;

theorem Th118: :: PBOOLE:118

for I being set
for Y, X being ManySortedSet of I holds Y misses X \ Y

proof end;

theorem :: PBOOLE:119

for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y

proof end;

theorem :: PBOOLE:120

for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \+\ Y

proof end;

theorem Th121: :: PBOOLE:121

for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X /\ Y = [[0]] I

proof end;

theorem :: PBOOLE:122

for I being set
for X being ManySortedSet of I st X <> [[0]] I holds
X meets X

proof end;

theorem :: PBOOLE:123

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y misses Z holds
X = [[0]] I

proof end;

theorem :: PBOOLE:124

for I being set
for Z, V, X, Y being ManySortedSet of I st Z \/ V = X \/ Y & X misses Z & Y misses V holds
( X = V & Y = Z )

proof end;

theorem :: PBOOLE:125

canceled;

theorem Th126: :: PBOOLE:126

for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X \ Y = X

proof end;

theorem :: PBOOLE:127

for I being set
for X, Y being ManySortedSet of I st X misses Y holds
(X \/ Y) \ Y = X

proof end;

theorem :: PBOOLE:128

for I being set
for X, Y being ManySortedSet of I st X \ Y = X holds
X misses Y

proof end;

theorem :: PBOOLE:129

for I being set
for X, Y being ManySortedSet of I holds X \ Y misses Y \ X

proof end;

begin

definition

let I be set ;
let X, Y be ManySortedSet of I;
pred X [= Y means :Def14: :: PBOOLE:def 14
for x being ManySortedSet of I st x in X holds
x in Y;
reflexivity ;

end;

:: deftheorem Def14 defines [= PBOOLE:def 14 :

theorem :: PBOOLE:130

for I being set
for X, Y being ManySortedSet of I st X c= Y holds
X [= Y

proof end;

theorem :: PBOOLE:131

canceled;

theorem :: PBOOLE:132

for I being set
for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z

proof end;

begin

theorem :: PBOOLE:133

[[0]] {} in [[0]] {}

proof end;

theorem :: PBOOLE:134

for X being ManySortedSet of {} holds X = {}

proof end;

theorem :: PBOOLE:135

for I being non empty set
for X, Y being ManySortedSet of I st X overlaps Y holds
X meets Y

proof end;

theorem Th136: :: PBOOLE:136

for I being non empty set
for x being ManySortedSet of I holds not x in [[0]] I

proof end;

theorem :: PBOOLE:137

for I being non empty set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X /\ Y <> [[0]] I

proof end;

theorem :: PBOOLE:138

for I being non empty set
for X being ManySortedSet of I holds not X overlaps [[0]] I

proof end;

theorem Th139: :: PBOOLE:139

for I being non empty set
for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds
not X overlaps Y

proof end;

theorem :: PBOOLE:140

for I being non empty set
for X being ManySortedSet of I st X overlaps X holds
X <> [[0]] I

proof end;

begin

definition

let I be set ;
let X be ManySortedSet of I;
:: original: empty-yielding
redefine attr X is empty-yielding means :Def15: :: PBOOLE:def 15
for i being set st i in I holds
X . i is empty ;
compatibility

proof end;

:: original: non-empty
redefine attr X is non-empty means :Def16: :: PBOOLE:def 16
for i being set st i in I holds
not X . i is empty ;
compatibility

proof end;

end;

:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :

:: deftheorem Def16 defines non-empty PBOOLE:def 16 :

registration

let I be set ;
cluster Relation-like V9() I -defined Function-like total set ;
existence

proof end;

cluster Relation-like V8() I -defined Function-like total set ;
existence

proof end;

end;

registration

let I be non empty set ;
cluster Relation-like V8() I -defined Function-like total -> V9() set ;
coherence

proof end;

cluster Relation-like V9() I -defined Function-like total -> V8() set ;
coherence ;

end;

theorem :: PBOOLE:141

for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff X = [[0]] I )

proof end;

theorem :: PBOOLE:142

for I being set
for Y, X being ManySortedSet of I st Y is empty-yielding & X c= Y holds
X is empty-yielding

proof end;

theorem Th143: :: PBOOLE:143

for I being set
for X, Y being ManySortedSet of I st X is non-empty & X c= Y holds
Y is non-empty

proof end;

theorem Th144: :: PBOOLE:144

for I being set
for X, Y being ManySortedSet of I st X is non-empty & X [= Y holds
X c= Y

proof end;

theorem :: PBOOLE:145

for I being set
for X, Y being ManySortedSet of I st X is non-empty & X [= Y holds
Y is non-empty

proof end;

theorem :: PBOOLE:146

for I being set
for X being V8() ManySortedSet of I ex x being ManySortedSet of I st x in X

proof end;

theorem Th147: :: PBOOLE:147

for I being set
for Y being ManySortedSet of I
for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) holds
X = Y

proof end;

theorem :: PBOOLE:148

for I being set
for Y, Z being ManySortedSet of I
for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) holds
X = Y /\ Z

proof end;

begin

scheme :: PBOOLE:sch 3
MSSEx{ F₁() -> set , P₁[ set , set ] } :

ex f being ManySortedSet of F₁() st
for i being set st i in F₁() holds
P₁[i,f . i]

provided

A1: for i being set st i in F₁() holds
ex j being set st P₁[i,j]

proof end;

scheme :: PBOOLE:sch 4
MSSLambda{ F₁() -> set , F₂( set ) -> set } :

ex f being ManySortedSet of F₁() st
for i being set st i in F₁() holds
f . i = F₂(i)

proof end;

registration

let I be set ;
cluster Relation-like I -defined Function-like total Function-yielding set ;
existence

proof end;

end;

definition

let I be set ;
mode ManySortedFunction of I is Function-yielding ManySortedSet of I;

end;

begin

theorem Th149: :: PBOOLE:149

for I being set
for M being V8() ManySortedSet of I holds not {} in rng M

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
mode Component of M is Element of rng M;

end;

theorem :: PBOOLE:150

for I being non empty set
for M being ManySortedSet of I
for A being Component of M ex i being set st
( i in I & A = M . i )

proof end;

theorem :: PBOOLE:151

for I being set
for M being ManySortedSet of I
for i being set st i in I holds
M . i is Component of M

proof end;

definition

let I be set ;
let B be ManySortedSet of I;
mode Element of B -> ManySortedSet of I means :: PBOOLE:def 17
for i being set st i in I holds
it . i is Element of B . i;
existence

proof end;

end;

:: deftheorem defines Element PBOOLE:def 17 :

begin

definition

let I be set ;
let A, B be ManySortedSet of I;
mode ManySortedFunction of A,B -> ManySortedSet of I means :Def18: :: PBOOLE:def 18
for i being set st i in I holds
it . i is Function of (A . i),(B . i);
correctness

proof end;

end;

:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :

registration

let I be set ;
let A, B be ManySortedSet of I;
cluster -> Function-yielding ManySortedFunction of A,B;
coherence

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
func M # -> ManySortedSet of I * means :Def19: :: PBOOLE:def 19
for i being Element of I * holds it . i = product (M * i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines # PBOOLE:def 19 :

registration

let I be set ;
let M be V8() ManySortedSet of I;
cluster M # -> V8() ;
coherence

proof end;

end;

registration

let I be set ;
let J be non empty set ;
let O be Function of I,J;
let F be ManySortedSet of J;
cluster O * F -> I -defined total I -defined Function;
coherence

proof end;

end;

definition

let a be set ;
func *--> a -> Function of NAT,({a} *) means :Def20: :: PBOOLE:def 20
for n being Element of NAT holds it . n = n |-> a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines *--> PBOOLE:def 20 :

theorem Th152: :: PBOOLE:152

for n being Element of NAT
for a, b being set holds (a .--> b) * (n |-> a) = n |-> b

proof end;

theorem :: PBOOLE:153

for D being non empty set
for n being Element of NAT
for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)

proof end;

scheme :: PBOOLE:sch 5
LambdaDMS{ F₁() -> non empty set , F₂( set ) -> set } :

ex X being ManySortedSet of F₁() st
for d being Element of F₁() holds X . d = F₂(d)

proof end;

registration

let J be non empty set ;
let B be V8() ManySortedSet of J;
let j be Element of J;
cluster B . j -> non empty ;
coherence by Def16;

end;

definition

let I be set ;
let X, Y be ManySortedSet of I;
func [|X,Y|] -> ManySortedSet of I means :: PBOOLE:def 21
for i being set st i in I holds
it . i = [:(X . i),(Y . i):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines [| PBOOLE:def 21 :

definition

let I be set ;
let X, Y be ManySortedSet of I;
deffunc H₁( set ) -> set = Funcs ((X . $1),(Y . $1));
func MSFuncs (X,Y) -> ManySortedSet of I means :: PBOOLE:def 22
for i being set st i in I holds
it . i = Funcs ((X . i),(Y . i));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines MSFuncs PBOOLE:def 22 :

definition

let I be set ;
let M be ManySortedSet of I;
mode ManySortedSubset of M -> ManySortedSet of I means :Def23: :: PBOOLE:def 23
it c= M;
existence ;

end;

:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :

registration

let I be set ;
let M be V8() ManySortedSet of I;
cluster Relation-like V8() I -defined Function-like total ManySortedSubset of M;
existence

proof end;

end;

definition

let F, G be Function-yielding Function;
func G ** F -> Function-yielding Function means :Def24: :: PBOOLE:def 24
( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds
it . i = (G . i) * (F . i) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines ** PBOOLE:def 24 :

definition

let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
func F .:.: A -> ManySortedSet of I means :: PBOOLE:def 25
for i being set st i in I holds
it . i = (F . i) .: (A . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines .:.: PBOOLE:def 25 :

registration

let I be set ;
cluster [[0]] I -> V9() ;
coherence

proof end;

end;

scheme :: PBOOLE:sch 6
MSSExD{ F₁() -> non empty set , P₁[ set , set ] } :

ex f being ManySortedSet of F₁() st
for i being Element of F₁() holds P₁[i,f . i]

provided

A1: for i being Element of F₁() ex j being set st P₁[i,j]

proof end;

registration

let A be non empty set ;
cluster Relation-like V8() A -defined Function-like total -> V9() set ;
coherence ;

end;

registration

let X be non empty set ;
cluster Relation-like X -defined Function-like total -> non empty set ;
coherence

proof end;

end;

theorem :: PBOOLE:154

for F, G, H being Function-yielding Function holds (H ** G) ** F = H ** (G ** F)

proof end;

registration

let I be set ;
let f be V8() ManySortedSet of I;
cluster Relation-like I -defined Function-like f -compatible total set ;
existence

proof end;

end;

theorem Th155: :: PBOOLE:155

for I being set
for f being V8() ManySortedSet of I
for s being b₂ -compatible ManySortedSet of I holds s in product f

proof end;

theorem :: PBOOLE:156

for I being set
for f being V8() ManySortedSet of I
for p being b₁ -defined b₂ -compatible Function ex s being b₂ -compatible ManySortedSet of I st p c= s

proof end;

registration

let I be set ;
let f be V8() ManySortedSet of I;
cluster -> total Element of product f;
coherence ;

end;

theorem :: PBOOLE:157

for I, A being set
for s, ss being ManySortedSet of I holds (ss +* (s | A)) | A = s | A

proof end;

definition

let I be set ;
let f be V8() ManySortedSet of I;
let M be f -compatible ManySortedSet of I;
func down M -> Element of product f equals :: PBOOLE:def 26
M;
coherence by Th155;

end;

:: deftheorem defines down PBOOLE:def 26 :

registration

let X be non empty set ;
let Y be set ;
cluster Relation-like Y -defined X -valued Function-like total set ;
existence

proof end;

end;

theorem :: PBOOLE:158

for I, Y being non empty set
for M being b₂ -valued ManySortedSet of I
for x being Element of I holds M . x = M /. x

proof end;

theorem :: PBOOLE:159

for F being NAT -defined total Function
for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i

proof end;