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

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 for set ;

existence
ex b₁ being I -defined Function st b₁ is total

proof end;

end;

definition

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

end;

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

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

provided

A1: for e being object 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 :: PBOOLE:def 1
for i being object st i in I holds
X . i in Y . i;

pred X c= Y means :: PBOOLE:def 2
for i being object st i in I holds
X . i c= Y . i;

reflexivity
for X being ManySortedSet of I
for i being object st i in I holds
X . i c= X . i ;

end;

:: deftheorem defines in PBOOLE:def 1 :
for I being set
for X, Y being ManySortedSet of I holds
( X in Y iff for i being object st i in I holds
X . i in Y . i );

:: deftheorem defines c= PBOOLE:def 2 :
for I being set
for X, Y being ManySortedSet of I holds
( X c= Y iff for i being object st i in I holds
X . i c= Y . i );

definition

let I be non empty set ;
let X, Y be ManySortedSet of I;
:: original: in
redefine pred X in Y;
asymmetry
for X, Y being ManySortedSet of I st (I,b₁,b₂) holds
not (I,b₂,b₁)

proof end;

end;

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

ex X being ManySortedSet of F₁() st
for i being object st i in F₁() holds
for e being object 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 object st i in I holds
X . i = Y . i ) holds
X = Y

proof end;

definition

let I be set ;

func EmptyMS I -> ManySortedSet of I equals :: PBOOLE:def 3
I --> {};

coherence
I --> {} is ManySortedSet of I ;
correctness
;
let X, Y be ManySortedSet of I;

func X (\/) Y -> ManySortedSet of I means :Def4: :: PBOOLE:def 4
for i being object st i in I holds
it . i = (X . i) \/ (Y . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = (X . i) \/ (Y . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (X . i) \/ (Y . i) ) & ( for i being object st i in I holds
b₂ . i = (X . i) \/ (Y . i) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, X, Y being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (X . i) \/ (Y . i) ) holds
for i being object st i in I holds
b₁ . i = (Y . i) \/ (X . i) ;
idempotence
for X being ManySortedSet of I
for i being object st i in I holds
X . i = (X . i) \/ (X . i) ;

func X (/\) Y -> ManySortedSet of I means :Def5: :: PBOOLE:def 5
for i being object st i in I holds
it . i = (X . i) /\ (Y . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = (X . i) /\ (Y . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (X . i) /\ (Y . i) ) & ( for i being object st i in I holds
b₂ . i = (X . i) /\ (Y . i) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, X, Y being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (X . i) /\ (Y . i) ) holds
for i being object st i in I holds
b₁ . i = (Y . i) /\ (X . i) ;
idempotence
for X being ManySortedSet of I
for i being object st i in I holds
X . i = (X . i) /\ (X . i) ;

func X (\) Y -> ManySortedSet of I means :Def6: :: PBOOLE:def 6
for i being object st i in I holds
it . i = (X . i) \ (Y . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = (X . i) \ (Y . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = (X . i) \ (Y . i) ) & ( for i being object st i in I holds
b₂ . i = (X . i) \ (Y . i) ) holds
b₁ = b₂

proof end;

pred X overlaps Y means :: PBOOLE:def 7
for i being object st i in I holds
X . i meets Y . i;

symmetry
for X, Y being ManySortedSet of I st ( for i being object st i in I holds
X . i meets Y . i ) holds
for i being object st i in I holds
Y . i meets X . i ;

pred X misses Y means :: PBOOLE:def 8
for i being object st i in I holds
X . i misses Y . i;

symmetry
for X, Y being ManySortedSet of I st ( for i being object st i in I holds
X . i misses Y . i ) holds
for i being object st i in I holds
Y . i misses X . i ;

end;

:: deftheorem defines EmptyMS PBOOLE:def 3 :
for I being set holds EmptyMS I = I --> {};

:: deftheorem Def4 defines (\/) PBOOLE:def 4 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = X (\/) Y iff for i being object st i in I holds
b₄ . i = (X . i) \/ (Y . i) );

:: deftheorem Def5 defines (/\) PBOOLE:def 5 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = X (/\) Y iff for i being object st i in I holds
b₄ . i = (X . i) /\ (Y . i) );

:: deftheorem Def6 defines (\) PBOOLE:def 6 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = X (\) Y iff for i being object st i in I holds
b₄ . i = (X . i) \ (Y . i) );

:: deftheorem defines overlaps PBOOLE:def 7 :
for I being set
for X, Y being ManySortedSet of I holds
( X overlaps Y iff for i being object st i in I holds
X . i meets Y . i );

:: deftheorem defines misses PBOOLE:def 8 :
for I being set
for X, Y being ManySortedSet of I holds
( X misses Y iff for i being object st i in I holds
X . i misses Y . i );

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 9
(X (\) Y) (\/) (Y (\) X);

correctness
coherence
(X (\) Y) (\/) (Y (\) X) is ManySortedSet of I;
;
commutativity
for b₁, X, Y being ManySortedSet of I st b₁ = (X (\) Y) (\/) (Y (\) X) holds
b₁ = (Y (\) X) (\/) (X (\) Y) ;

end;

:: deftheorem defines (\+\) PBOOLE:def 9 :
for I being set
for X, Y being ManySortedSet of I holds X (\+\) Y = (X (\) Y) (\/) (Y (\) X);

theorem Th4: :: PBOOLE:4

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

proof end;

theorem :: PBOOLE:5

for I being set
for i being object holds (EmptyMS I) . i = {} ;

theorem Th6: :: PBOOLE:6

for I being set
for X being ManySortedSet of I st ( for i being object st i in I holds
X . i = {} ) holds
X = EmptyMS 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;

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

proof end;

definition

let I be set ;
let X, Y be ManySortedSet of I;

:: original: =
redefine pred X = Y means :: PBOOLE:def 10
for i being object st i in I holds
X . i = Y . i;

compatibility
( X = Y iff for i being object st i in I holds
X . i = Y . i ) by Th3;

end;

:: deftheorem defines = PBOOLE:def 10 :
for I being set
for X, Y being ManySortedSet of I holds
( X = Y iff for i being object st i in I holds
X . i = Y . i );

theorem Th13: :: PBOOLE:13

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 Th14: :: PBOOLE:14

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

proof end;

theorem Th15: :: PBOOLE:15

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

proof end;

theorem Th16: :: PBOOLE:16

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

proof end;

theorem Th17: :: PBOOLE:17

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

proof end;

theorem :: PBOOLE:18

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 Th19: :: PBOOLE:19

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 Th20: :: PBOOLE:20

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:21

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 Th22: :: PBOOLE:22

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

proof end;

theorem Th23: :: PBOOLE:23

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

proof end;

theorem :: PBOOLE:24

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

proof end;

theorem :: PBOOLE:25

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

proof end;

theorem :: PBOOLE:26

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:27

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 Th28: :: PBOOLE:28

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

proof end;

theorem Th29: :: PBOOLE:29

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

proof end;

theorem Th30: :: PBOOLE:30

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

proof end;

theorem Th31: :: PBOOLE:31

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

proof end;

theorem Th32: :: PBOOLE:32

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

proof end;

theorem Th33: :: PBOOLE:33

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

proof end;

theorem :: PBOOLE:34

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:35

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:36

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:37

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

proof end;

theorem :: PBOOLE:38

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

proof end;

theorem :: PBOOLE:39

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

proof end;

theorem :: PBOOLE:40

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

proof end;

theorem :: PBOOLE:41

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

proof end;

theorem :: PBOOLE:42

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

proof end;

theorem Th43: :: PBOOLE:43

for I being set
for X being ManySortedSet of I holds EmptyMS I c= X

proof end;

theorem Th44: :: PBOOLE:44

for I being set
for X being ManySortedSet of I st X c= EmptyMS I holds
X = EmptyMS I

proof end;

theorem :: PBOOLE:45

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y (/\) Z = EmptyMS I holds
X = EmptyMS I by Th17, Th44;

theorem :: PBOOLE:46

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y (/\) Z = EmptyMS I holds
X (/\) Z = EmptyMS I by Th44, Th19;

theorem :: PBOOLE:47

for I being set
for X being ManySortedSet of I holds
( X (\/) (EmptyMS I) = X & (EmptyMS I) (\/) X = X ) by Th22, Th43;

theorem :: PBOOLE:48

for I being set
for X, Y being ManySortedSet of I st X (\/) Y = EmptyMS I holds
X = EmptyMS I by Th44, Th14;

theorem :: PBOOLE:49

for I being set
for X being ManySortedSet of I holds X (/\) (EmptyMS I) = EmptyMS I by Th23, Th43;

theorem :: PBOOLE:50

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

proof end;

theorem :: PBOOLE:51

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

theorem Th52: :: PBOOLE:52

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

proof end;

theorem Th53: :: PBOOLE:53

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 Th54: :: PBOOLE:54

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:55

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 Th56: :: PBOOLE:56

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

proof end;

theorem :: PBOOLE:57

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

proof end;

theorem :: PBOOLE:58

for I being set
for X being ManySortedSet of I holds X (\) X = EmptyMS I by Th52;

theorem Th59: :: PBOOLE:59

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

proof end;

theorem Th60: :: PBOOLE:60

for I being set
for X being ManySortedSet of I holds (EmptyMS I) (\) X = EmptyMS I by Th43, Th52;

theorem :: PBOOLE:61

for I being set
for X, Y being ManySortedSet of I holds X (\) (X (\/) Y) = EmptyMS I by Th14, Th52;

theorem Th62: :: PBOOLE:62

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

proof end;

theorem Th63: :: PBOOLE:63

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

proof end;

theorem Th64: :: PBOOLE:64

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

proof end;

theorem Th65: :: PBOOLE:65

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

proof end;

theorem :: PBOOLE:66

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

proof end;

theorem Th67: :: PBOOLE:67

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

proof end;

theorem Th68: :: PBOOLE:68

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

proof end;

theorem Th69: :: PBOOLE:69

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

proof end;

theorem Th70: :: PBOOLE:70

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

proof end;

theorem :: PBOOLE:71

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

proof end;

theorem Th72: :: PBOOLE:72

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

proof end;

theorem Th73: :: PBOOLE:73

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

proof end;

theorem :: PBOOLE:74

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

proof end;

theorem Th75: :: PBOOLE:75

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

proof end;

theorem :: PBOOLE:76

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 Th77: :: PBOOLE:77

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

proof end;

theorem Th78: :: PBOOLE:78

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

proof end;

theorem :: PBOOLE:79

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

proof end;

theorem :: PBOOLE:80

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

proof end;

theorem :: PBOOLE:81

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

proof end;

theorem :: PBOOLE:82

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:83

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

theorem :: PBOOLE:84

for I being set
for X being ManySortedSet of I holds X (\+\) (EmptyMS I) = X

proof end;

theorem :: PBOOLE:85

for I being set
for X being ManySortedSet of I holds X (\+\) X = EmptyMS I by Th52;

theorem :: PBOOLE:86

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

proof end;

theorem Th87: :: PBOOLE:87

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

proof end;

theorem :: PBOOLE:88

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:89

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 Th90: :: PBOOLE:90

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

proof end;

theorem :: PBOOLE:91

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 Th16;

theorem Th92: :: PBOOLE:92

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

proof end;

theorem Th93: :: PBOOLE:93

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

proof end;

theorem Th94: :: PBOOLE:94

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

proof end;

theorem Th95: :: PBOOLE:95

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

proof end;

theorem :: PBOOLE:96

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

proof end;

theorem :: PBOOLE:97

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

proof end;

theorem :: PBOOLE:98

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 Th99: :: PBOOLE:99

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 Th100: :: PBOOLE:100

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 Th101: :: PBOOLE:101

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:102

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:103

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:104

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y (\) Z holds
X overlaps Y by Th56, Th99;

theorem :: PBOOLE:105

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

proof end;

theorem :: PBOOLE:106

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 Th107: :: PBOOLE:107

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 Th108: :: PBOOLE:108

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

proof end;

theorem :: PBOOLE:109

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

proof end;

theorem :: PBOOLE:110

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

proof end;

theorem Th111: :: PBOOLE:111

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

proof end;

theorem :: PBOOLE:112

for I being set
for X being ManySortedSet of I st X <> EmptyMS I holds
X meets X

proof end;

theorem :: PBOOLE:113

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

proof end;

theorem :: PBOOLE:114

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

proof end;

theorem Th115: :: PBOOLE:115

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

proof end;

theorem :: PBOOLE:116

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

proof end;

theorem :: PBOOLE:117

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

proof end;

theorem :: PBOOLE:118

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

proof end;

definition

let I be set ;
let X, Y be ManySortedSet of I;

pred X [= Y means :: PBOOLE:def 11
for x being ManySortedSet of I st x in X holds
x in Y;

reflexivity
for X, x being ManySortedSet of I st x in X holds
x in X ;

end;

:: deftheorem defines [= PBOOLE:def 11 :
for I being set
for X, Y being ManySortedSet of I holds
( X [= Y iff for x being ManySortedSet of I st x in X holds
x in Y );

theorem :: PBOOLE:119

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

proof end;

theorem :: PBOOLE:120

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

theorem :: PBOOLE:121

EmptyMS {} in EmptyMS {} ;

theorem :: PBOOLE:122

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

theorem :: PBOOLE:123

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

proof end;

theorem Th124: :: PBOOLE:124

for I being non empty set
for x being ManySortedSet of I holds not x in EmptyMS I

proof end;

theorem :: PBOOLE:125

for I being non empty set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X (/\) Y <> EmptyMS I by Th8, Th124;

theorem :: PBOOLE:126

for I being non empty set
for X being ManySortedSet of I holds not X overlaps EmptyMS I

proof end;

theorem Th127: :: PBOOLE:127

for I being non empty set
for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds
not X overlaps Y

proof end;

theorem :: PBOOLE:128

for I being non empty set
for X being ManySortedSet of I st X overlaps X holds
X <> EmptyMS I

proof end;

definition

let I be set ;
let X be ManySortedSet of I;

:: original: empty-yielding
redefine attr X is empty-yielding means :: PBOOLE:def 12
for i being object st i in I holds
X . i is empty ;

compatibility
( X is empty-yielding iff for i being object st i in I holds
X . i is empty )

proof end;

:: original: non-empty
redefine attr X is non-empty means :Def13: :: PBOOLE:def 13
for i being object st i in I holds
not X . i is empty ;

compatibility
( X is non-empty iff for i being object st i in I holds
not X . i is empty )

proof end;

end;

:: deftheorem defines empty-yielding PBOOLE:def 12 :
for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff for i being object st i in I holds
X . i is empty );

:: deftheorem Def13 defines non-empty PBOOLE:def 13 :
for I being set
for X being ManySortedSet of I holds
( X is non-empty iff for i being object st i in I holds
not X . i is empty );

registration

let I be set ;

cluster Relation-like V9() I -defined Function-like total for set ;

existence
not for b₁ being ManySortedSet of I holds b₁ is V9()

proof end;

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

existence
not for b₁ being ManySortedSet of I holds b₁ is V8()

proof end;

end;

registration

let I be non empty set ;

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

coherence
for b₁ being ManySortedSet of I st b₁ is V8() holds
not b₁ is V9()

proof end;

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

coherence
for b₁ being ManySortedSet of I st b₁ is V9() holds
not b₁ is V8() ;

end;

theorem :: PBOOLE:129

for I being set
for X being ManySortedSet of I holds
( X is V9() iff X = EmptyMS I )

proof end;

theorem :: PBOOLE:130

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

proof end;

theorem Th131: :: PBOOLE:131

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

proof end;

theorem Th132: :: PBOOLE:132

for I being set
for X, Y being ManySortedSet of I st X is V8() & X [= Y holds
X c= Y

proof end;

theorem :: PBOOLE:133

for I being set
for X, Y being ManySortedSet of I st X is V8() & X [= Y holds
Y is V8()

proof end;

theorem :: PBOOLE:134

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

proof end;

theorem Th135: :: PBOOLE:135

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:136

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;

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

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

provided

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

proof end;

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

ex f being ManySortedSet of F₁() st
for i being object 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 for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is Function-yielding

proof end;

end;

definition

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

end;

theorem :: PBOOLE:137

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

proof end;

definition

let M be Function;
mode Component of M is Element of rng M;

end;

theorem :: PBOOLE:138

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

proof end;

theorem :: PBOOLE:139

for I being set
for M being ManySortedSet of I
for i being object 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 14
for i being object st i in I holds
it . i is Element of B . i;

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i is Element of B . i

proof end;

end;

:: deftheorem defines Element PBOOLE:def 14 :
for I being set
for B, b₃ being ManySortedSet of I holds
( b₃ is Element of B iff for i being object st i in I holds
b₃ . i is Element of B . i );

definition

let I be set ;
let A, B be ManySortedSet of I;

mode ManySortedFunction of A,B -> ManySortedSet of I means :Def15: :: PBOOLE:def 15
for i being object st i in I holds
it . i is Function of (A . i),(B . i);

correctness
existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i is Function of (A . i),(B . i);

proof end;

end;

:: deftheorem Def15 defines ManySortedFunction PBOOLE:def 15 :
for I being set
for A, B, b₄ being ManySortedSet of I holds
( b₄ is ManySortedFunction of A,B iff for i being object st i in I holds
b₄ . i is Function of (A . i),(B . i) );

registration

let I be set ;
let A, B be ManySortedSet of I;

cluster -> Function-yielding for ManySortedFunction of A,B;

coherence
for b₁ being ManySortedFunction of A,B holds b₁ is Function-yielding

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 for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = F * O holds
b₁ is total

proof end;

end;

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

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
not B . j is empty by Def13;

end;

definition

let I be set ;
let X, Y be ManySortedSet of I;

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

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = [:(X . i),(Y . i):]

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = [:(X . i),(Y . i):] ) & ( for i being object st i in I holds
b₂ . i = [:(X . i),(Y . i):] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines [| PBOOLE:def 16 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = [|X,Y|] iff for i being object st i in I holds
b₄ . i = [:(X . i),(Y . i):] );

definition

let I be set ;
let X, Y be ManySortedSet of I;
deffunc H₁( object ) -> set = Funcs ((X . $1),(Y . $1));

func (Funcs) (X,Y) -> ManySortedSet of I means :: PBOOLE:def 17
for i being object st i in I holds
it . i = Funcs ((X . i),(Y . i));

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = Funcs ((X . i),(Y . i))

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = Funcs ((X . i),(Y . i)) ) & ( for i being object st i in I holds
b₂ . i = Funcs ((X . i),(Y . i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines (Funcs) PBOOLE:def 17 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = (Funcs) (X,Y) iff for i being object st i in I holds
b₄ . i = Funcs ((X . i),(Y . i)) );

definition

let I be set ;
let M be ManySortedSet of I;

mode ManySortedSubset of M -> ManySortedSet of I means :Def18: :: PBOOLE:def 18
it c= M;

existence
ex b₁ being ManySortedSet of I st b₁ c= M ;

end;

:: deftheorem Def18 defines ManySortedSubset PBOOLE:def 18 :
for I being set
for M, b₃ being ManySortedSet of I holds
( b₃ is ManySortedSubset of M iff b₃ c= M );

registration

let I be set ;
let M be V8() ManySortedSet of I;

cluster Relation-like V8() I -defined Function-like total for ManySortedSubset of M;

existence
not for b₁ being ManySortedSubset of M holds b₁ is V8()

proof end;

end;

definition

let F, G be Function-yielding Function;

func G ** F -> Function means :Def19: :: PBOOLE:def 19
( dom it = (dom F) /\ (dom G) & ( for i being object st i in dom it holds
it . i = (G . i) * (F . i) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom F) /\ (dom G) & ( for i being object st i in dom b₁ holds
b₁ . i = (G . i) * (F . i) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom F) /\ (dom G) & ( for i being object st i in dom b₁ holds
b₁ . i = (G . i) * (F . i) ) & dom b₂ = (dom F) /\ (dom G) & ( for i being object st i in dom b₂ holds
b₂ . i = (G . i) * (F . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines ** PBOOLE:def 19 :
for F, G being Function-yielding Function
for b₃ being Function holds
( b₃ = G ** F iff ( dom b₃ = (dom F) /\ (dom G) & ( for i being object st i in dom b₃ holds
b₃ . i = (G . i) * (F . i) ) ) );

registration

let F, G be Function-yielding Function;

cluster G ** F -> Function-yielding ;

coherence
G ** F is Function-yielding

proof end;

end;

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 20
for i being set st i in I holds
it . i = (F . i) .: (A . i);

existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
b₁ . i = (F . i) .: (A . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being set st i in I holds
b₁ . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds
b₂ . i = (F . i) .: (A . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines .:.: PBOOLE:def 20 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b₄ being ManySortedSet of I holds
( b₄ = F .:.: A iff for i being set st i in I holds
b₄ . i = (F . i) .: (A . i) );

registration

let I be set ;

cluster EmptyMS I -> V9() ;

coherence
EmptyMS I is empty-yielding ;

end;

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

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 object st P₁[i,j]

proof end;

registration

let A be non empty set ;

cluster Relation-like V8() A -defined Function-like total -> V9() for set ;

coherence
for b₁ being ManySortedSet of A st b₁ is V8() holds
not b₁ is V9() ;

end;

registration

let X be non empty set ;

cluster Relation-like X -defined Function-like total -> non empty for set ;

coherence
for b₁ being ManySortedSet of X holds not b₁ is empty ;

end;

theorem :: PBOOLE:140

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 for set ;

existence
ex b₁ being I -defined f -compatible Function st b₁ is total

proof end;

end;

theorem :: PBOOLE:141

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;

theorem :: PBOOLE:142

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

proof end;

registration

let X be non empty set ;
let Y be set ;

cluster Relation-like Y -defined X -valued Function-like total for set ;

existence
ex b₁ being ManySortedSet of Y st b₁ is X -valued

proof end;

end;

theorem :: PBOOLE:143

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:144

for I being set
for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M

proof end;

theorem :: PBOOLE:145

for I being set
for Y being non empty set
for p being b₁ -defined b₂ -valued Function ex s being b₂ -valued ManySortedSet of I st p c= s

proof end;

theorem :: PBOOLE:146

for I being set
for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y by Lm1;

definition

let I be non empty set ;
let A, B be ManySortedSet of I;

:: original: =
redefine pred A = B means :: PBOOLE:def 21
for i being Element of I holds A . i = B . i;

compatibility
( A = B iff for i being Element of I holds A . i = B . i ) ;

end;

:: deftheorem defines = PBOOLE:def 21 :
for I being non empty set
for A, B being ManySortedSet of I holds
( A = B iff for i being Element of I holds A . i = B . i );

registration

let X be with_non-empty_elements set ;

cluster id X -> non-empty ;

coherence
id X is non-empty by SETFAM_1:def 8;

end;

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

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

proof end;