:: Manysorted Sets
:: by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-2012 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 = {{}} ) )
proofend;

registration
let I be set ;
cluster Relation-like I -defined Function-like total for set ;
existence
 ex b1 being I -defined Function st b1 is total
proofend;
end;

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

scheme :: PBOOLE:sch 1
KuratowskiFunction{ F1() ->  set , F2( set ) ->  set } :
 ex f being ManySortedSet of F1() st
for e being set st e in F1() holds
f . e in F2(e)
provided
A1: for e being set st e in F1() holds
F2(e) <> {}
proofend;

definition
let I be set ;
let X, Y be ManySortedSet of I;
predX in Y means :Def1: :: PBOOLE:def 1
 for i being set st i in I holds
X . i in Y . i;
predX c= Y means :Def2: :: PBOOLE:def 2
 for i being set st i in I holds
X . i c= Y . i;
reflexivity
 for X being ManySortedSet of I
for i being set st i in I holds
X . i c= X . i ;
end;

:: deftheorem Def1 defines in PBOOLE:def_1_:_
 for I being set
for X, Y being ManySortedSet of I holds
( X in Y iff for i being set st i in I holds
X . i in Y . i );

:: deftheorem Def2 defines c= PBOOLE:def_2_:_
 for I being set
for X, Y being ManySortedSet of I holds
( X c= Y iff for i being set 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 predX in Y;
asymmetry
 for X, Y being ManySortedSet of I st (I,b1,b2) holds
not (I,b2,b1)
proofend;
end;

scheme :: PBOOLE:sch 2
PSeparation{ F1() ->  set , F2() ->  ManySortedSet of F1(), P1[ set , set ] } :
 ex X being ManySortedSet of F1() st
for i being set st i in F1() holds
for e being set holds
( e in X . i iff ( e in F2() . i &amp; P1[i,e] ) )
proofend;

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

definition
let I be set ;
func [[0]] I ->  ManySortedSet of I equals :: PBOOLE:def 3
I --> {};
coherence
 I --> {} is ManySortedSet of I ;
correctness
;
let X, Y be ManySortedSet of I;
funcX \/ Y ->  ManySortedSet of I means :Def4: :: PBOOLE:def 4
 for i being set st i in I holds
it . i = (X . i) \/ (Y . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) &amp; ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
proofend;
commutativity
 for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) \/ (X . i) ;
idempotence
 for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) \/ (X . i) ;
funcX /\ Y ->  ManySortedSet of I means :Def5: :: PBOOLE:def 5
 for i being set st i in I holds
it . i = (X . i) /\ (Y . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) &amp; ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
proofend;
commutativity
 for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) /\ (X . i) ;
idempotence
 for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) /\ (X . i) ;
funcX \ Y ->  ManySortedSet of I means :Def6: :: PBOOLE:def 6
 for i being set st i in I holds
it . i = (X . i) \ (Y . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) &amp; ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
proofend;
predX overlaps Y means :Def7: :: PBOOLE:def 7
 for i being set st i in I holds
X . i meets Y . i;
symmetry
 for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i meets Y . i ) holds
for i being set st i in I holds
Y . i meets X . i ;
predX misses Y means :Def8: :: PBOOLE:def 8
 for i being set st i in I holds
X . i misses Y . i;
symmetry
 for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i misses Y . i ) holds
for i being set st i in I holds
Y . i misses X . i ;
end;

:: deftheorem  defines [[0]] PBOOLE:def_3_:_
 for I being set holds [[0]] I = I --> {};

:: deftheorem Def4 defines \/ PBOOLE:def_4_:_
 for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \/ Y iff for i being set st i in I holds
b4 . i = (X . i) \/ (Y . i) );

:: deftheorem Def5 defines /\ PBOOLE:def_5_:_
 for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X /\ Y iff for i being set st i in I holds
b4 . i = (X . i) /\ (Y . i) );

:: deftheorem Def6 defines \ PBOOLE:def_6_:_
 for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \ Y iff for i being set st i in I holds
b4 . i = (X . i) \ (Y . i) );

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

:: deftheorem Def8 defines misses PBOOLE:def_8_:_
 for I being set
for X, Y being ManySortedSet of I holds
( X misses Y iff for i being set 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;
funcX \+\ Y ->  ManySortedSet of I equals :: PBOOLE:def 9
(X \ Y) \/ (Y \ X);
correctness
coherence
(X \ Y) \/ (Y \ X) is ManySortedSet of I;
;
commutativity
 for b1, X, Y being ManySortedSet of I st b1 = (X \ Y) \/ (Y \ X) holds
b1 = (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 set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
proofend;

theorem Th5: :: PBOOLE:5
for i, I being set holds ([[0]] I) . i = {}
proofend;

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

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

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 &amp; x in Y ) )
proofend;

theorem Th9: :: PBOOLE:9
for I being set
for x, X, Y being ManySortedSet of I st x in X &amp; X c= Y holds
x in Y
proofend;

theorem Th10: :: PBOOLE:10
for I being set
for x, X, Y being ManySortedSet of I st x in X &amp; x in Y holds
X overlaps Y
proofend;

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 &amp; x in Y )
proofend;

theorem :: PBOOLE:12
for I being set
for x, X, Y being ManySortedSet of I st x in X \ Y holds
x in X
proofend;

begin

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

definition
let I be set ;
let X, Y be ManySortedSet of I;
:: original:=
redefine predX = Y means :: PBOOLE:def 10
 for i being set st i in I holds
X . i = Y . i;
compatibility
 ( X = Y iff for i being set 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 set 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 &amp; Y c= Z holds
X c= Z
proofend;

theorem Th14: :: PBOOLE:14
for I being set
for X, Y being ManySortedSet of I holds X c= X \/ Y
proofend;

theorem Th15: :: PBOOLE:15
for I being set
for X, Y being ManySortedSet of I holds X /\ Y c= X
proofend;

theorem Th16: :: PBOOLE:16
for I being set
for X, Z, Y being ManySortedSet of I st X c= Z &amp; Y c= Z holds
X \/ Y c= Z
proofend;

theorem Th17: :: PBOOLE:17
for I being set
for Z, X, Y being ManySortedSet of I st Z c= X &amp; Z c= Y holds
Z c= X /\ Y
proofend;

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

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

theorem Th20: :: PBOOLE:20
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y &amp; Z c= V holds
X \/ Z c= Y \/ V
proofend;

theorem :: PBOOLE:21
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y &amp; Z c= V holds
X /\ Z c= Y /\ V
proofend;

theorem Th22: :: PBOOLE:22
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
X \/ Y = Y
proofend;

theorem Th23: :: PBOOLE:23
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
X /\ Y = X
proofend;

theorem :: PBOOLE:24
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z
proofend;

theorem :: PBOOLE:25
for I being set
for X, Z, Y being ManySortedSet of I st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
proofend;

theorem :: PBOOLE:26
for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y \/ Z iff ( Y c= X &amp; Z c= X &amp; ( for V being ManySortedSet of I st Y c= V &amp; Z c= V holds
X c= V ) ) )
proofend;

theorem :: PBOOLE:27
for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y /\ Z iff ( X c= Y &amp; X c= Z &amp; ( for V being ManySortedSet of I st V c= Y &amp; V c= Z holds
V c= X ) ) )
proofend;

theorem Th28: :: PBOOLE:28
for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = X \/ (Y \/ Z)
proofend;

theorem Th29: :: PBOOLE:29
for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = X /\ (Y /\ Z)
proofend;

theorem Th30: :: PBOOLE:30
for I being set
for X, Y being ManySortedSet of I holds X /\ (X \/ Y) = X
proofend;

theorem Th31: :: PBOOLE:31
for I being set
for X, Y being ManySortedSet of I holds X \/ (X /\ Y) = X
proofend;

theorem Th32: :: PBOOLE:32
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
proofend;

theorem Th33: :: PBOOLE:33
for I being set
for X, Y, Z being ManySortedSet of I holds X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
proofend;

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

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

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)
proofend;

theorem :: PBOOLE:37
for I being set
for X, Y, Z being ManySortedSet of I st X \/ Y c= Z holds
X c= Z
proofend;

theorem :: PBOOLE:38
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y /\ Z holds
X c= Y
proofend;

theorem :: PBOOLE:39
for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proofend;

theorem :: PBOOLE:40
for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = (X /\ Z) /\ (Y /\ Z)
proofend;

theorem :: PBOOLE:41
for I being set
for X, Y being ManySortedSet of I holds X \/ (X \/ Y) = X \/ Y
proofend;

theorem :: PBOOLE:42
for I being set
for X, Y being ManySortedSet of I holds X /\ (X /\ Y) = X /\ Y
proofend;

begin

theorem Th43: :: PBOOLE:43
for I being set
for X being ManySortedSet of I holds [[0]] I c= X
proofend;

theorem Th44: :: PBOOLE:44
for I being set
for X being ManySortedSet of I st X c= [[0]] I holds
X = [[0]] I
proofend;

theorem :: PBOOLE:45
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y &amp; X c= Z &amp; Y /\ Z = [[0]] I holds
X = [[0]] I by Th17, Th44;

theorem :: PBOOLE:46
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y &amp; Y /\ Z = [[0]] I holds
X /\ Z = [[0]] I by Th44, Th19;

theorem :: PBOOLE:47
for I being set
for X being ManySortedSet of I holds
( X \/ ([[0]] I) = X &amp; ([[0]] I) \/ X = X ) by Th22, Th43;

theorem :: PBOOLE:48
for I being set
for X, Y being ManySortedSet of I st X \/ Y = [[0]] I holds
X = [[0]] I by Th44, Th14;

theorem :: PBOOLE:49
for I being set
for X being ManySortedSet of I holds X /\ ([[0]] I) = [[0]] I by Th23, Th43;

theorem :: PBOOLE:50
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y \/ Z &amp; X /\ Z = [[0]] I holds
X c= Y
proofend;

theorem :: PBOOLE:51
for I being set
for Y, X being ManySortedSet of I st Y c= X &amp; X /\ Y = [[0]] I holds
Y = [[0]] I by Th23;

begin

theorem Th52: :: PBOOLE:52
for I being set
for X, Y being ManySortedSet of I holds
( X \ Y = [[0]] I iff X c= Y )
proofend;

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

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

theorem :: PBOOLE:55
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y &amp; Z c= V holds
X \ V c= Y \ Z
proofend;

theorem Th56: :: PBOOLE:56
for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X
proofend;

theorem :: PBOOLE:57
for I being set
for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [[0]] I
proofend;

theorem :: PBOOLE:58
for I being set
for X being ManySortedSet of I holds X \ X = [[0]] I by Th52;

theorem Th59: :: PBOOLE:59
for I being set
for X being ManySortedSet of I holds X \ ([[0]] I) = X
proofend;

theorem Th60: :: PBOOLE:60
for I being set
for X being ManySortedSet of I holds ([[0]] I) \ X = [[0]] I
proofend;

theorem :: PBOOLE:61
for I being set
for X, Y being ManySortedSet of I holds X \ (X \/ Y) = [[0]] I
proofend;

theorem Th62: :: PBOOLE:62
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ Z
proofend;

theorem Th63: :: PBOOLE:63
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) /\ Y = [[0]] I
proofend;

theorem Th64: :: PBOOLE:64
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
proofend;

theorem Th65: :: PBOOLE:65
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \/ (X /\ Y) = X
proofend;

theorem :: PBOOLE:66
for I being set
for X, Y being ManySortedSet of I st X c= Y holds
Y = X \/ (Y \ X)
proofend;

theorem Th67: :: PBOOLE:67
for I being set
for X, Y being ManySortedSet of I holds X \/ (Y \ X) = X \/ Y
proofend;

theorem Th68: :: PBOOLE:68
for I being set
for X, Y being ManySortedSet of I holds X \ (X \ Y) = X /\ Y
proofend;

theorem Th69: :: PBOOLE:69
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proofend;

theorem Th70: :: PBOOLE:70
for I being set
for X, Y being ManySortedSet of I holds X \ (X /\ Y) = X \ Y
proofend;

theorem :: PBOOLE:71
for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y = [[0]] I iff X \ Y = X )
proofend;

theorem Th72: :: PBOOLE:72
for I being set
for X, Y, Z being ManySortedSet of I holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proofend;

theorem Th73: :: PBOOLE:73
for I being set
for X, Y, Z being ManySortedSet of I holds (X \ Y) \ Z = X \ (Y \/ Z)
proofend;

theorem :: PBOOLE:74
for I being set
for X, Y, Z being ManySortedSet of I holds (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z)
proofend;

theorem Th75: :: PBOOLE:75
for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y
proofend;

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 &amp; X \ Z c= Y )
proofend;

theorem Th77: :: PBOOLE:77
for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proofend;

theorem Th78: :: PBOOLE:78
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y
proofend;

theorem :: PBOOLE:79
for I being set
for X, Y, Z being ManySortedSet of I holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proofend;

theorem :: PBOOLE:80
for I being set
for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y
proofend;

theorem :: PBOOLE:81
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
proofend;

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

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 \+\ ([[0]] I) = X
proofend;

theorem :: PBOOLE:85
for I being set
for X being ManySortedSet of I holds X \+\ X = [[0]] I by Th52;

theorem :: PBOOLE:86
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \/ (X /\ Y)
proofend;

theorem Th87: :: PBOOLE:87
for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \/ Y) \ (X /\ Y)
proofend;

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))
proofend;

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)
proofend;

theorem Th90: :: PBOOLE:90
for I being set
for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proofend;

theorem :: PBOOLE:91
for I being set
for X, Y, Z being ManySortedSet of I st X \ Y c= Z &amp; 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)
proofend;

theorem Th93: :: PBOOLE:93
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = X \+\ (X \ Y)
proofend;

theorem Th94: :: PBOOLE:94
for I being set
for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)
proofend;

theorem Th95: :: PBOOLE:95
for I being set
for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)
proofend;

theorem :: PBOOLE:96
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
proofend;

theorem :: PBOOLE:97
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
proofend;

begin

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

theorem Th99: :: PBOOLE:99
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y &amp; Y c= Z holds
X overlaps Z
proofend;

theorem Th100: :: PBOOLE:100
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y &amp; X c= Z holds
Z overlaps Y
proofend;

theorem Th101: :: PBOOLE:101
for I being set
for X, Y, Z, V being ManySortedSet of I st X c= Y &amp; Z c= V &amp; X overlaps Z holds
Y overlaps V
proofend;

theorem :: PBOOLE:102
for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y /\ Z holds
( X overlaps Y &amp; X overlaps Z )
proofend;

theorem :: PBOOLE:103
for I being set
for X, Z, V being ManySortedSet of I st X overlaps Z &amp; X c= V holds
X overlaps Z /\ V
proofend;

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 Y, Z, X being ManySortedSet of I st not Y overlaps Z holds
not X /\ Y overlaps X /\ Z
proofend;

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

theorem Th107: :: PBOOLE:107
for I being set
for X, Y, Z being ManySortedSet of I st X meets Y &amp; Y c= Z holds
X meets Z
proofend;

theorem Th108: :: PBOOLE:108
for I being set
for Y, X being ManySortedSet of I holds Y misses X \ Y
proofend;

theorem :: PBOOLE:109
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y
proofend;

theorem :: PBOOLE:110
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \+\ Y
proofend;

theorem Th111: :: PBOOLE:111
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X /\ Y = [[0]] I
proofend;

theorem :: PBOOLE:112
for I being set
for X being ManySortedSet of I st X <> [[0]] I holds
X meets X
proofend;

theorem :: PBOOLE:113
for I being set
for X, Y, Z being ManySortedSet of I st X c= Y &amp; X c= Z &amp; Y misses Z holds
X = [[0]] I
proofend;

theorem :: PBOOLE:114
for I being set
for Z, V, X, Y being ManySortedSet of I st Z \/ V = X \/ Y &amp; X misses Z &amp; Y misses V holds
( X = V &amp; Y = Z )
proofend;

theorem Th115: :: PBOOLE:115
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X \ Y = X
proofend;

theorem :: PBOOLE:116
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
(X \/ Y) \ Y = X
proofend;

theorem :: PBOOLE:117
for I being set
for X, Y being ManySortedSet of I st X \ Y = X holds
X misses Y
proofend;

theorem :: PBOOLE:118
for I being set
for X, Y being ManySortedSet of I holds X \ Y misses Y \ X
proofend;

begin

definition
let I be set ;
let X, Y be ManySortedSet of I;
predX [= Y means :Def11: :: 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 Def11 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
proofend;

theorem :: PBOOLE:120
for I being set
for X, Y, Z being ManySortedSet of I st X [= Y &amp; Y [= Z holds
X [= Z
proofend;

begin

theorem :: PBOOLE:121
[[0]] {} in [[0]] {}
proofend;

theorem :: PBOOLE:122
for X being ManySortedSet of {} holds X = {}
proofend;

theorem :: PBOOLE:123
for I being non empty set
for X, Y being ManySortedSet of I st X overlaps Y holds
X meets Y
proofend;

theorem Th124: :: PBOOLE:124
for I being non empty set
for x being ManySortedSet of I holds not x in [[0]] I
proofend;

theorem :: PBOOLE:125
for I being non empty set
for x, X, Y being ManySortedSet of I st x in X &amp; x in Y holds
X /\ Y <> [[0]] I
proofend;

theorem :: PBOOLE:126
for I being non empty set
for X being ManySortedSet of I holds not X overlaps [[0]] I
proofend;

theorem Th127: :: PBOOLE:127
for I being non empty set
for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds
not X overlaps Y
proofend;

theorem :: PBOOLE:128
for I being non empty set
for X being ManySortedSet of I st X overlaps X holds
X <> [[0]] I
proofend;

begin

definition
let I be set ;
let X be ManySortedSet of I;
:: original:empty-yielding
redefine attrX is empty-yielding  means :: PBOOLE:def 12
 for i being set st i in I holds
X . i is empty ;
compatibility
 ( X is empty-yielding iff for i being set st i in I holds
X . i is empty )
proofend;
:: original:non-empty
redefine attrX is non-empty  means :Def13: :: PBOOLE:def 13
 for i being set st i in I holds
not X . i is empty ;
compatibility
 ( X is non-empty iff for i being set st i in I holds
not X . i is empty )
proofend;
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 set 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 set 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 b1 being ManySortedSet of I holds b1 is V9()
proofend;
cluster Relation-like V8() I -defined Function-like total for set ;
existence
 not for b1 being ManySortedSet of I holds b1 is V8()
proofend;
end;

registration
let I be non empty set ;
cluster Relation-like V8() I -defined Function-like total  -> V9() for set ;
coherence
 for b1 being ManySortedSet of I st b1 is V8() holds
not b1 is V9()
proofend;
cluster Relation-like V9() I -defined Function-like total  -> V8() for set ;
coherence
 for b1 being ManySortedSet of I st b1 is V9() holds
not b1 is V8() ;
end;

theorem :: PBOOLE:129
for I being set
for X being ManySortedSet of I holds
( X is V9() iff X = [[0]] I )
proofend;

theorem :: PBOOLE:130
for I being set
for Y, X being ManySortedSet of I st Y is V9() &amp; X c= Y holds
X is V9()
proofend;

theorem Th131: :: PBOOLE:131
for I being set
for X, Y being ManySortedSet of I st X is V8() &amp; X c= Y holds
Y is V8()
proofend;

theorem Th132: :: PBOOLE:132
for I being set
for X, Y being ManySortedSet of I st X is V8() &amp; X [= Y holds
X c= Y
proofend;

theorem :: PBOOLE:133
for I being set
for X, Y being ManySortedSet of I st X is V8() &amp; X [= Y holds
Y is V8()
proofend;

theorem :: PBOOLE:134
for I being set
for X being V8() ManySortedSet of I ex x being ManySortedSet of I st x in X
proofend;

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

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 &amp; x in Z ) ) ) holds
X = Y /\ Z
proofend;

begin

scheme :: PBOOLE:sch 3
MSSEx{ F1() ->  set , P1[ set , set ] } :
 ex f being ManySortedSet of F1() st
for i being set st i in F1() holds
P1[i,f . i]
provided
A1: for i being set st i in F1() holds
ex j being set st P1[i,j]
proofend;

scheme :: PBOOLE:sch 4
MSSLambda{ F1() ->  set , F2( set ) ->  set } :
 ex f being ManySortedSet of F1() st
for i being set st i in F1() holds
f . i = F2(i)
proofend;

registration
let I be set ;
cluster Relation-like I -defined Function-like total Function-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is Function-yielding
proofend;
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
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
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 set st
( i in I &amp; A = M . i )
proofend;

theorem :: PBOOLE:139
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
proofend;

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 set st i in I holds
it . i is Element of B . i;
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Element of B . i
proofend;
end;

:: deftheorem  defines Element PBOOLE:def_14_:_
 for I being set
for B, b3 being ManySortedSet of I holds
( b3 is Element of B iff for i being set st i in I holds
b3 . i is Element of B . i );

begin

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 set st i in I holds
it . i is Function of (A . i),(B . i);
correctness
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Function of (A . i),(B . i);
proofend;
end;

:: deftheorem Def15 defines ManySortedFunction PBOOLE:def_15_:_
 for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedFunction of A,B iff for i being set st i in I holds
b4 . 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 b1 being ManySortedFunction of A,B holds b1 is Function-yielding
proofend;
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;
clusterO * F -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = F * O holds
b1 is total
proofend;
end;

scheme :: PBOOLE:sch 5
LambdaDMS{ F1() ->  non empty set , F2( set ) ->  set } :
 ex X being ManySortedSet of F1() st
for d being Element of F1() holds X . d = F2(d)
proofend;

registration
let J be non empty set ;
let B be V8() ManySortedSet of J;
let j be Element of J;
clusterB . 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 set st i in I holds
it . i = [:(X . i),(Y . i):];
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = [:(X . i),(Y . i):]
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = [:(X . i),(Y . i):] ) &amp; ( for i being set st i in I holds
b2 . i = [:(X . i),(Y . i):] ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines [| PBOOLE:def_16_:_
 for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = [|X,Y|] iff for i being set st i in I holds
b4 . i = [:(X . i),(Y . i):] );

definition
let I be set ;
let X, Y be ManySortedSet of I;
deffunc H1( set ) ->  set = Funcs ((X . $1),(Y . $1));
func (Funcs) (X,Y) ->  ManySortedSet of I means :: PBOOLE:def 17
 for i being set st i in I holds
it . i = Funcs ((X . i),(Y . i));
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = Funcs ((X . i),(Y . i))
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = Funcs ((X . i),(Y . i)) ) &amp; ( for i being set st i in I holds
b2 . i = Funcs ((X . i),(Y . i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines (Funcs) PBOOLE:def_17_:_
 for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = (Funcs) (X,Y) iff for i being set st i in I holds
b4 . 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 b1 being ManySortedSet of I st b1 c= M ;
end;

:: deftheorem Def18 defines ManySortedSubset PBOOLE:def_18_:_
 for I being set
for M, b3 being ManySortedSet of I holds
( b3 is ManySortedSubset of M iff b3 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 b1 being ManySortedSubset of M holds b1 is V8()
proofend;
end;

definition
let F, G be Function-yielding Function;
funcG ** F ->  Function means :Def19: :: PBOOLE:def 19
( dom it = (dom F) /\ (dom G) &amp; ( for i being set st i in dom it holds
it . i = (G . i) * (F . i) ) );
existence
 ex b1 being Function st
( dom b1 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) &amp; dom b2 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b2 holds
b2 . i = (G . i) * (F . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines ** PBOOLE:def_19_:_
 for F, G being Function-yielding Function
for b3 being Function holds
( b3 = G ** F iff ( dom b3 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b3 holds
b3 . i = (G . i) * (F . i) ) ) );

registration
let F, G be Function-yielding Function;
clusterG ** F ->  Function-yielding ;
coherence
 G ** F is Function-yielding
proofend;
end;

definition
let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
funcF .:.: 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 b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (F . i) .: (A . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (F . i) .: (A . i) ) &amp; ( for i being set st i in I holds
b2 . i = (F . i) .: (A . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines .:.: PBOOLE:def_20_:_
 for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F .:.: A iff for i being set st i in I holds
b4 . i = (F . i) .: (A . i) );

registration
let I be set ;
cluster [[0]] I -> V9() ;
coherence
 [[0]] I is empty-yielding
proofend;
end;

scheme :: PBOOLE:sch 6
MSSExD{ F1() ->  non empty set , P1[ set , set ] } :
 ex f being ManySortedSet of F1() st
for i being Element of F1() holds P1[i,f . i]
provided
A1: for i being Element of F1() ex j being set st P1[i,j]
proofend;

registration
let A be non empty set ;
cluster Relation-like V8() A -defined Function-like total  -> V9() for set ;
coherence
 for b1 being ManySortedSet of A st b1 is V8() holds
not b1 is V9() ;
end;

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total  ->  non empty for set ;
coherence
 for b1 being ManySortedSet of X holds not b1 is empty
proofend;
end;

theorem :: PBOOLE:140
for F, G, H being Function-yielding Function holds (H ** G) ** F = H ** (G ** F)
proofend;

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 b1 being I -defined f -compatible Function st b1 is total
proofend;
end;

theorem :: PBOOLE:141
for I being set
for f being V8() ManySortedSet of I
for p being b1 -defined b2 -compatible Function ex s being b2 -compatible ManySortedSet of I st p c= s
proofend;

theorem :: PBOOLE:142
for I, A being set
for s, ss being ManySortedSet of I holds (ss +* (s | A)) | A = s | A
proofend;

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 b1 being ManySortedSet of Y st b1 is X -valued
proofend;
end;

theorem :: PBOOLE:143
for I, Y being non empty set
for M being b2 -valued ManySortedSet of I
for x being Element of I holds M . x = M /. x
proofend;

theorem :: PBOOLE:144
for I being set
for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M
proofend;

theorem :: PBOOLE:145
for I being set
for Y being non empty set
for p being b1 -defined b2 -valued Function ex s being b2 -valued ManySortedSet of I st p c= s
proofend;

theorem :: PBOOLE:146
for I being set
for X, Y being ManySortedSet of I st X c= Y &amp; Y c= X holds
X = Y by Lm1;

definition
let I be non empty set ;
let A, B be ManySortedSet of I;
:: original:=
redefine predA = 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 )
proofend;
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 );