:: PBOOLE semantic presentation

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
let f be Function; ::_thesis: ( f is empty-yielding iff ( f = {} or rng f = {{}} ) )
hereby  ::_thesis: ( ( f = {} or rng f = {{}} ) implies f is empty-yielding )
assume that
A1: f is empty-yielding and
A2: f <> {} ; ::_thesis: rng f = {{}}
thus  rng f = {{}} ::_thesis: verum
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= rng f
let i be set ; ::_thesis: ( i in rng f implies i in {{}} )
assume  i in rng f ; ::_thesis: i in {{}}
then  ex e being set st
( e in dom f & f . e = i ) by FUNCT_1:def_3;
then  i = {} by A1;
hence  i in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set e = the Element of dom f;
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in {{}} or i in rng f )
assume  i in {{}} ; ::_thesis: i in rng f
then A3: i = {} by TARSKI:def_1;
A4: dom f <> {} by A2, RELAT_1:41;
 f . the Element of dom f is empty by A1;
hence  i in rng f by A4, A3, FUNCT_1:def_3; ::_thesis: verum
end;
end;
assume A5: ( f = {} or rng f = {{}} ) ; ::_thesis: f is empty-yielding
percases ( f = {} or rng f = {{}} ) by A5;
suppose f = {} ; ::_thesis: f is empty-yielding
hence  for i being set st i in dom f holds
f . i is empty by RELAT_1:38; :: according to FUNCT_1:def_8 ::_thesis: verum
end;
supposeA6: rng f = {{}} ; ::_thesis: f is empty-yielding
let i be set ; :: according to FUNCT_1:def_8 ::_thesis: ( not i in dom f or f . i is empty )
assume  i in dom f ; ::_thesis: f . i is empty
then  f . i in rng f by FUNCT_1:def_3;
hence  f . i is empty by A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;

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
proof
take  I --> {} ; ::_thesis: I --> {} is total
thus  I --> {} is total ; ::_thesis: verum
end;
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) <> {}
proof
defpred S1[ set , set ] means $2 in F2($1);
A2: now__::_thesis:_for_e_being_set_st_e_in_F1()_holds_
ex_fe_being_set_st_S1[e,fe]
let e be set ; ::_thesis: ( e in F1() implies ex fe being set st S1[e,fe] )
set fe = the Element of F2(e);
assume A3: e in F1() ; ::_thesis: ex fe being set st S1[e,fe]
reconsider fe = the Element of F2(e) as set ;
take fe = fe; ::_thesis: S1[e,fe]
 F2(e) <> {} by A1, A3;
hence  S1[e,fe] ; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = F1() and
A5: for e being set st e in F1() holds
S1[e,f . e] from CLASSES1:sch_1(A2);
reconsider f = f as ManySortedSet of F1() by A4, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for e being set st e in F1() holds
f . e in F2(e)
thus  for e being set st e in F1() holds
f . e in F2(e) by A5; ::_thesis: verum
end;

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)
proof
let X, Y be ManySortedSet of I; ::_thesis: ( (I,X,Y) implies not (I,Y,X) )
assume A1: for i being set st i in I holds
X . i in Y . i ; :: according to PBOOLE:def_1 ::_thesis: (I,Y,X)
 ex i being set st
( i in I & not Y . i in X . i )
proof
assume A2: for i being set st i in I holds
Y . i in X . i ; ::_thesis: contradiction
consider i being set  such that
A3: i in I by XBOOLE_0:def_1;
 X . i in Y . i by A1, A3;
hence  contradiction by A2, A3; ::_thesis: verum
end;
hence  (I,Y,X) by Def1; ::_thesis: verum
end;
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 & P1[i,e] ) )
proof
defpred S1[ set , set ] means  for e being set holds
( e in $2 iff ( e in F2() . $1 & P1[$1,e] ) );
A1: now__::_thesis:_for_i_being_set_st_i_in_F1()_holds_
ex_u_being_set_st_S1[i,u]
let i be set ; ::_thesis: ( i in F1() implies ex u being set st S1[i,u] )
assume  i in F1() ; ::_thesis: ex u being set st S1[i,u]
defpred S2[ set ] means P1[i,$1];
 ex u being set st
for e being set holds
( e in u iff ( e in F2() . i & S2[e] ) ) from XBOOLE_0:sch_1();
hence  ex u being set st S1[i,u] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = F1() and
A3: for i being set st i in F1() holds
S1[i,f . i] from CLASSES1:sch_1(A1);
 f is ManySortedSet of F1() by A2, PARTFUN1:def_2, RELAT_1:def_18;
hence  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 & P1[i,e] ) ) by A3; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i = Y . i ) holds
X = Y
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = Y . i ) implies X = Y )
 ( dom X = I & dom Y = I ) by PARTFUN1:def_2;
hence  ( ( for i being set st i in I holds
X . i = Y . i ) implies X = Y ) by FUNCT_1:2; ::_thesis: verum
end;

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)
proof
deffunc H1( set ) ->  set = (X . $1) \/ (Y . $1);
consider f being Function such that
A1: dom f = I and
A2: for i being set st i in I holds
f . i = H1(i) from FUNCT_1:sch_3();
 f is ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18;
hence  ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
proof
let A1, A2 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
A1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
A2 . i = (X . i) \/ (Y . i) ) implies A1 = A2 )
assume that
A3: for i being set st i in I holds
A1 . i = (X . i) \/ (Y . i) and
A4: for i being set st i in I holds
A2 . i = (X . i) \/ (Y . i) ; ::_thesis: A1 = A2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A1_._i_=_A2_._i
let i be set ; ::_thesis: ( i in I implies A1 . i = A2 . i )
assume A5: i in I ; ::_thesis: A1 . i = A2 . i
hence A1 . i = (X . i) \/ (Y . i) by A3
.= A2 . i by A4, A5 ;
::_thesis: verum
end;
hence  A1 = A2 by Th3; ::_thesis: verum
end;
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)
proof
deffunc H1( set ) ->  set = (X . $1) /\ (Y . $1);
consider f being Function such that
A6: dom f = I and
A7: for i being set st i in I holds
f . i = H1(i) from FUNCT_1:sch_3();
 f is ManySortedSet of I by A6, PARTFUN1:def_2, RELAT_1:def_18;
hence  ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
proof
let A1, A2 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
A1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
A2 . i = (X . i) /\ (Y . i) ) implies A1 = A2 )
assume that
A8: for i being set st i in I holds
A1 . i = (X . i) /\ (Y . i) and
A9: for i being set st i in I holds
A2 . i = (X . i) /\ (Y . i) ; ::_thesis: A1 = A2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A1_._i_=_A2_._i
let i be set ; ::_thesis: ( i in I implies A1 . i = A2 . i )
assume A10: i in I ; ::_thesis: A1 . i = A2 . i
hence A1 . i = (X . i) /\ (Y . i) by A8
.= A2 . i by A9, A10 ;
::_thesis: verum
end;
hence  A1 = A2 by Th3; ::_thesis: verum
end;
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)
proof
deffunc H1( set ) ->  Element of bool (X . $1) = (X . $1) \ (Y . $1);
consider f being Function such that
A11: dom f = I and
A12: for i being set st i in I holds
f . i = H1(i) from FUNCT_1:sch_3();
 f is ManySortedSet of I by A11, PARTFUN1:def_2, RELAT_1:def_18;
hence  ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) by A12; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
proof
let A1, A2 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
A1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
A2 . i = (X . i) \ (Y . i) ) implies A1 = A2 )
assume that
A13: for i being set st i in I holds
A1 . i = (X . i) \ (Y . i) and
A14: for i being set st i in I holds
A2 . i = (X . i) \ (Y . i) ; ::_thesis: A1 = A2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
A1_._i_=_A2_._i
let i be set ; ::_thesis: ( i in I implies A1 . i = A2 . i )
assume A15: i in I ; ::_thesis: A1 . i = A2 . i
hence A1 . i = (X . i) \ (Y . i) by A13
.= A2 . i by A14, A15 ;
::_thesis: verum
end;
hence  A1 = A2 by Th3; ::_thesis: verum
end;
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)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I
for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
let X, Y be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
let i be set ; ::_thesis: ( i in I implies (X \+\ Y) . i = (X . i) \+\ (Y . i) )
assume A1: i in I ; ::_thesis: (X \+\ Y) . i = (X . i) \+\ (Y . i)
thus (X \+\ Y) . i = ((X \ Y) . i) \/ ((Y \ X) . i) by A1, Def4
.= ((X . i) \ (Y . i)) \/ ((Y \ X) . i) by A1, Def6
.= (X . i) \+\ (Y . i) by A1, Def6 ; ::_thesis: verum
end;

theorem Th5: :: PBOOLE:5
for i, I being set holds ([[0]] I) . i = {}
proof
let i, I be set ; ::_thesis: ([[0]] I) . i = {}
percases ( i in I or not i in I ) ;
suppose i in I ; ::_thesis: ([[0]] I) . i = {}
hence  ([[0]] I) . i = {} by FUNCOP_1:7; ::_thesis: verum
end;
suppose not i in I ; ::_thesis: ([[0]] I) . i = {}
then  not i in dom ([[0]] I) by FUNCOP_1:13;
hence  ([[0]] I) . i = {} by FUNCT_1:def_2; ::_thesis: verum
end;
end;
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
let I be set ; ::_thesis: for X being ManySortedSet of I st ( for i being set st i in I holds
X . i = {} ) holds
X = [[0]] I
let X be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = {} ) implies X = [[0]] I )
assume A1: for i being set st i in I holds
X . i = {} ; ::_thesis: X = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_([[0]]_I)_._i
let i be set ; ::_thesis: ( i in I implies X . i = ([[0]] I) . i )
assume  i in I ; ::_thesis: X . i = ([[0]] I) . i
hence X . i = {} by A1
.= ([[0]] I) . i by Th5 ;
::_thesis: verum
end;
hence  X = [[0]] I by Th3; ::_thesis: verum
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
let I be set ; ::_thesis: for x, X, Y being ManySortedSet of I st ( x in X or x in Y ) holds
x in X \/ Y
let x, X, Y be ManySortedSet of I; ::_thesis: ( ( x in X or x in Y ) implies x in X \/ Y )
assume A1: ( x in X or x in Y ) ; ::_thesis: x in X \/ Y
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in (X \/ Y) . i )
assume A2: i in I ; ::_thesis: x . i in (X \/ Y) . i
then  ( x . i in X . i or x . i in Y . i ) by A1, Def1;
then  x . i in (X . i) \/ (Y . i) by XBOOLE_0:def_3;
hence  x . i in (X \/ Y) . i by A2, Def4; ::_thesis: verum
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
let I be set ; ::_thesis: for x, X, Y being ManySortedSet of I holds
( x in X /\ Y iff ( x in X & x in Y ) )
let x, X, Y be ManySortedSet of I; ::_thesis: ( x in X /\ Y iff ( x in X & x in Y ) )
hereby  ::_thesis: ( x in X & x in Y implies x in X /\ Y )
assume A1: x in X /\ Y ; ::_thesis: ( x in X & x in Y )
thus  x in X ::_thesis: x in Y
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in X . i )
assume A2: i in I ; ::_thesis: x . i in X . i
then  x . i in (X /\ Y) . i by A1, Def1;
then  x . i in (X . i) /\ (Y . i) by A2, Def5;
hence  x . i in X . i by XBOOLE_0:def_4; ::_thesis: verum
end;
thus  x in Y ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in Y . i )
assume A3: i in I ; ::_thesis: x . i in Y . i
then  x . i in (X /\ Y) . i by A1, Def1;
then  x . i in (X . i) /\ (Y . i) by A3, Def5;
hence  x . i in Y . i by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A4: ( x in X & x in Y ) ; ::_thesis: x in X /\ Y
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in (X /\ Y) . i )
assume A5: i in I ; ::_thesis: x . i in (X /\ Y) . i
then  ( x . i in X . i & x . i in Y . i ) by A4, Def1;
then  x . i in (X . i) /\ (Y . i) by XBOOLE_0:def_4;
hence  x . i in (X /\ Y) . i by A5, Def5; ::_thesis: verum
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
let I be set ; ::_thesis: for x, X, Y being ManySortedSet of I st x in X & X c= Y holds
x in Y
let x, X, Y be ManySortedSet of I; ::_thesis: ( x in X & X c= Y implies x in Y )
assume A1: ( x in X & X c= Y ) ; ::_thesis: x in Y
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in Y . i )
assume  i in I ; ::_thesis: x . i in Y . i
then  ( x . i in X . i & X . i c= Y . i ) by A1, Def1, Def2;
hence  x . i in Y . i ; ::_thesis: verum
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
let I be set ; ::_thesis: for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlaps Y
let x, X, Y be ManySortedSet of I; ::_thesis: ( x in X & x in Y implies X overlaps Y )
assume A1: ( x in X & x in Y ) ; ::_thesis: X overlaps Y
let i be set ; :: according to PBOOLE:def_7 ::_thesis: ( i in I implies X . i meets Y . i )
assume  i in I ; ::_thesis: X . i meets Y . i
then  ( x . i in X . i & x . i in Y . i ) by A1, Def1;
hence  X . i meets Y . i by XBOOLE_0:3; ::_thesis: verum
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
let I be set ; ::_thesis: 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 )
let X, Y be ManySortedSet of I; ::_thesis: ( X overlaps Y implies ex x being ManySortedSet of I st
( x in X & x in Y ) )
deffunc H1( set ) ->  set = (X . $1) /\ (Y . $1);
assume A1: X overlaps Y ; ::_thesis: ex x being ManySortedSet of I st
( x in X & x in Y )
A2: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
H1(i)_<>_{}
let i be set ; ::_thesis: ( i in I implies H1(i) <> {} )
assume  i in I ; ::_thesis: H1(i) <> {}
then  X . i meets Y . i by A1, Def7;
hence  H1(i) <> {} by XBOOLE_0:def_7; ::_thesis: verum
end;
consider x being ManySortedSet of I such that
A3: for i being set st i in I holds
x . i in H1(i) from PBOOLE:sch_1(A2);
take  x ; ::_thesis: ( x in X & x in Y )
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
x_._i_in_X_._i
let i be set ; ::_thesis: ( i in I implies x . i in X . i )
assume  i in I ; ::_thesis: x . i in X . i
then  x . i in (X . i) /\ (Y . i) by A3;
hence  x . i in X . i by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in X by Def1; ::_thesis: x in Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
x_._i_in_Y_._i
let i be set ; ::_thesis: ( i in I implies x . i in Y . i )
assume  i in I ; ::_thesis: x . i in Y . i
then  x . i in (X . i) /\ (Y . i) by A3;
hence  x . i in Y . i by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in Y by Def1; ::_thesis: verum
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
let I be set ; ::_thesis: for x, X, Y being ManySortedSet of I st x in X \ Y holds
x in X
let x, X, Y be ManySortedSet of I; ::_thesis: ( x in X \ Y implies x in X )
assume A1: x in X \ Y ; ::_thesis: x in X
thus  x in X ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in X . i )
assume A2: i in I ; ::_thesis: x . i in X . i
then  x . i in (X \ Y) . i by A1, Def1;
then  x . i in (X . i) \ (Y . i) by A2, Def6;
hence  x . i in X . i ; ::_thesis: verum
end;
end;

begin

Lm1:  for I being set
for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y & Y c= X implies X = Y )
assume A1: ( X c= Y & Y c= X ) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume  i in I ; ::_thesis: X . i = Y . i
then  ( X . i c= Y . i & Y . i c= X . i ) by A1, Def2;
hence  X . i = Y . i by XBOOLE_0:def_10; ::_thesis: verum
end;
hence  X = Y by Th3; ::_thesis: verum
end;

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 & Y c= Z holds
X c= Z
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y & Y c= Z holds
X c= Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y & Y c= Z implies X c= Z )
assume that
A1: X c= Y and
A2: Y c= Z ; ::_thesis: X c= Z
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies X . i c= Z . i )
assume A3: i in I ; ::_thesis: X . i c= Z . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X . i or e in Z . i )
assume A4: e in X . i ; ::_thesis: e in Z . i
 X . i c= Y . i by A1, A3, Def2;
then A5: e in Y . i by A4;
 Y . i c= Z . i by A2, A3, Def2;
hence  e in Z . i by A5; ::_thesis: verum
end;

theorem Th14: :: PBOOLE:14
for I being set
for X, Y being ManySortedSet of I holds X c= X \/ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X c= X \/ Y
let X, Y be ManySortedSet of I; ::_thesis: X c= X \/ Y
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies X . i c= (X \/ Y) . i )
assume A1: i in I ; ::_thesis: X . i c= (X \/ Y) . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X . i or e in (X \/ Y) . i )
assume  e in X . i ; ::_thesis: e in (X \/ Y) . i
then  e in (X . i) \/ (Y . i) by XBOOLE_0:def_3;
hence  e in (X \/ Y) . i by A1, Def4; ::_thesis: verum
end;

theorem Th15: :: PBOOLE:15
for I being set
for X, Y being ManySortedSet of I holds X /\ Y c= X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ Y c= X
let X, Y be ManySortedSet of I; ::_thesis: X /\ Y c= X
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies (X /\ Y) . i c= X . i )
assume A1: i in I ; ::_thesis: (X /\ Y) . i c= X . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (X /\ Y) . i or e in X . i )
assume  e in (X /\ Y) . i ; ::_thesis: e in X . i
then  e in (X . i) /\ (Y . i) by A1, Def5;
hence  e in X . i by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th16: :: PBOOLE:16
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
let I be set ; ::_thesis: for X, Z, Y being ManySortedSet of I st X c= Z & Y c= Z holds
X \/ Y c= Z
let X, Z, Y be ManySortedSet of I; ::_thesis: ( X c= Z & Y c= Z implies X \/ Y c= Z )
assume A1: ( X c= Z & Y c= Z ) ; ::_thesis: X \/ Y c= Z
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies (X \/ Y) . i c= Z . i )
assume A2: i in I ; ::_thesis: (X \/ Y) . i c= Z . i
then  ( X . i c= Z . i & Y . i c= Z . i ) by A1, Def2;
then  (X . i) \/ (Y . i) c= Z . i by XBOOLE_1:8;
hence  (X \/ Y) . i c= Z . i by A2, Def4; ::_thesis: verum
end;

theorem Th17: :: PBOOLE:17
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
let I be set ; ::_thesis: for Z, X, Y being ManySortedSet of I st Z c= X & Z c= Y holds
Z c= X /\ Y
let Z, X, Y be ManySortedSet of I; ::_thesis: ( Z c= X & Z c= Y implies Z c= X /\ Y )
assume A1: ( Z c= X & Z c= Y ) ; ::_thesis: Z c= X /\ Y
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies Z . i c= (X /\ Y) . i )
assume A2: i in I ; ::_thesis: Z . i c= (X /\ Y) . i
then  ( Z . i c= X . i & Z . i c= Y . i ) by A1, Def2;
then  Z . i c= (X . i) /\ (Y . i) by XBOOLE_1:19;
hence  Z . i c= (X /\ Y) . i by A2, Def5; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
X \/ Z c= Y \/ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y implies X \/ Z c= Y \/ Z )
assume A1: X c= Y ; ::_thesis: X \/ Z c= Y \/ Z
A2: Z c= Y \/ Z by Th14;
 Y c= Y \/ Z by Th14;
then  X c= Y \/ Z by A1, Th13;
hence  X \/ Z c= Y \/ Z by A2, Th16; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
X /\ Z c= Y /\ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y implies X /\ Z c= Y /\ Z )
assume A1: X c= Y ; ::_thesis: X /\ Z c= Y /\ Z
A2: X /\ Z c= Z by Th15;
 X /\ Z c= X by Th15;
then  X /\ Z c= Y by A1, Th13;
hence  X /\ Z c= Y /\ Z by A2, Th17; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \/ Z c= Y \/ V
let X, Y, Z, V be ManySortedSet of I; ::_thesis: ( X c= Y & Z c= V implies X \/ Z c= Y \/ V )
assume that
A1: X c= Y and
A2: Z c= V ; ::_thesis: X \/ Z c= Y \/ V
 V c= Y \/ V by Th14;
then A3: Z c= Y \/ V by A2, Th13;
 Y c= Y \/ V by Th14;
then  X c= Y \/ V by A1, Th13;
hence  X \/ Z c= Y \/ V by A3, Th16; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X /\ Z c= Y /\ V
let X, Y, Z, V be ManySortedSet of I; ::_thesis: ( X c= Y & Z c= V implies X /\ Z c= Y /\ V )
assume that
A1: X c= Y and
A2: Z c= V ; ::_thesis: X /\ Z c= Y /\ V
 X /\ Z c= Z by Th15;
then A3: X /\ Z c= V by A2, Th13;
 X /\ Z c= X by Th15;
then  X /\ Z c= Y by A1, Th13;
hence  X /\ Z c= Y /\ V by A3, Th17; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y holds
X \/ Y = Y
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y implies X \/ Y = Y )
assume  X c= Y ; ::_thesis: X \/ Y = Y
then A1: X \/ Y c= Y by Th16;
 Y c= X \/ Y by Th14;
hence  X \/ Y = Y by A1, Lm1; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y holds
X /\ Y = X
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y implies X /\ Y = X )
assume A1: X c= Y ; ::_thesis: X /\ Y = X
A2: X /\ Y c= X by Th15;
 X c= X /\ Y by A1, Th17;
hence  X /\ Y = X by A2, Lm1; ::_thesis: verum
end;

theorem :: PBOOLE:24
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: X /\ Y c= X \/ Z
 ( X /\ Y c= X & X c= X \/ Z ) by Th14, Th15;
hence  X /\ Y c= X \/ Z by Th13; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for X, Z, Y being ManySortedSet of I st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
let X, Z, Y be ManySortedSet of I; ::_thesis: ( X c= Z implies X \/ (Y /\ Z) = (X \/ Y) /\ Z )
assume A1: X c= Z ; ::_thesis: X \/ (Y /\ Z) = (X \/ Y) /\ Z
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X \/ (Y /\ Z)) . i = ((X \/ Y) /\ Z) . i )
assume A2: i in I ; ::_thesis: (X \/ (Y /\ Z)) . i = ((X \/ Y) /\ Z) . i
then A3: X . i c= Z . i by A1, Def2;
thus (X \/ (Y /\ Z)) . i = (X . i) \/ ((Y /\ Z) . i) by A2, Def4
.= (X . i) \/ ((Y . i) /\ (Z . i)) by A2, Def5
.= ((X . i) \/ (Y . i)) /\ (Z . i) by A3, XBOOLE_1:30
.= ((X \/ Y) . i) /\ (Z . i) by A2, Def4
.= ((X \/ Y) /\ Z) . i by A2, Def5 ; ::_thesis: verum
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
let I be set ; ::_thesis: 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 ) ) )
let X, Y, Z be ManySortedSet of I; ::_thesis: ( 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 ) ) )
thus  ( X = Y \/ Z implies ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) ) by Th14, Th16; ::_thesis: ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) implies X = Y \/ Z )
assume that
A1: ( Y c= X & Z c= X ) and
A2: for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ; ::_thesis: X = Y \/ Z
 ( Y c= Y \/ Z & Z c= Y \/ Z ) by Th14;
then A3: X c= Y \/ Z by A2;
 Y \/ Z c= X by A1, Th16;
hence  X = Y \/ Z by A3, Lm1; ::_thesis: verum
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
let I be set ; ::_thesis: 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 ) ) )
let X, Y, Z be ManySortedSet of I; ::_thesis: ( 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 ) ) )
thus  ( X = Y /\ Z implies ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) ) by Th15, Th17; ::_thesis: ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) implies X = Y /\ Z )
assume that
A1: ( X c= Y & X c= Z ) and
A2: for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ; ::_thesis: X = Y /\ Z
A3: X c= Y /\ Z by A1, Th17;
 ( Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X ) by A2;
hence  X = Y /\ Z by A3, Lm1, Th15; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = X \/ (Y \/ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \/ Y) \/ Z = X \/ (Y \/ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies ((X \/ Y) \/ Z) . i = (X \/ (Y \/ Z)) . i )
assume A1: i in I ; ::_thesis: ((X \/ Y) \/ Z) . i = (X \/ (Y \/ Z)) . i
hence ((X \/ Y) \/ Z) . i = ((X \/ Y) . i) \/ (Z . i) by Def4
.= ((X . i) \/ (Y . i)) \/ (Z . i) by A1, Def4
.= (X . i) \/ ((Y . i) \/ (Z . i)) by XBOOLE_1:4
.= (X . i) \/ ((Y \/ Z) . i) by A1, Def4
.= (X \/ (Y \/ Z)) . i by A1, Def4 ;
::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = X /\ (Y /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X /\ Y) /\ Z = X /\ (Y /\ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies ((X /\ Y) /\ Z) . i = (X /\ (Y /\ Z)) . i )
assume A1: i in I ; ::_thesis: ((X /\ Y) /\ Z) . i = (X /\ (Y /\ Z)) . i
hence ((X /\ Y) /\ Z) . i = ((X /\ Y) . i) /\ (Z . i) by Def5
.= ((X . i) /\ (Y . i)) /\ (Z . i) by A1, Def5
.= (X . i) /\ ((Y . i) /\ (Z . i)) by XBOOLE_1:16
.= (X . i) /\ ((Y /\ Z) . i) by A1, Def5
.= (X /\ (Y /\ Z)) . i by A1, Def5 ;
::_thesis: verum
end;

theorem Th30: :: PBOOLE:30
for I being set
for X, Y being ManySortedSet of I holds X /\ (X \/ Y) = X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ (X \/ Y) = X
let X, Y be ManySortedSet of I; ::_thesis: X /\ (X \/ Y) = X
 X c= X \/ Y by Th14;
then A1: X c= X /\ (X \/ Y) by Th17;
 X /\ (X \/ Y) c= X by Th15;
hence  X /\ (X \/ Y) = X by A1, Lm1; ::_thesis: verum
end;

theorem Th31: :: PBOOLE:31
for I being set
for X, Y being ManySortedSet of I holds X \/ (X /\ Y) = X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ (X /\ Y) = X
let X, Y be ManySortedSet of I; ::_thesis: X \/ (X /\ Y) = X
 X /\ Y c= X by Th15;
then A1: X \/ (X /\ Y) c= X by Th16;
 X c= X \/ (X /\ Y) by Th14;
hence  X \/ (X /\ Y) = X by A1, Lm1; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X /\ (Y \/ Z)) . i = ((X /\ Y) \/ (X /\ Z)) . i )
assume A1: i in I ; ::_thesis: (X /\ (Y \/ Z)) . i = ((X /\ Y) \/ (X /\ Z)) . i
hence (X /\ (Y \/ Z)) . i = (X . i) /\ ((Y \/ Z) . i) by Def5
.= (X . i) /\ ((Y . i) \/ (Z . i)) by A1, Def4
.= ((X . i) /\ (Y . i)) \/ ((X . i) /\ (Z . i)) by XBOOLE_1:23
.= ((X /\ Y) . i) \/ ((X . i) /\ (Z . i)) by A1, Def5
.= ((X /\ Y) . i) \/ ((X /\ Z) . i) by A1, Def5
.= ((X /\ Y) \/ (X /\ Z)) . i by A1, Def4 ;
::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
thus X \/ (Y /\ Z) = (X \/ (X /\ Z)) \/ (Y /\ Z) by Th31
.= X \/ ((X /\ Z) \/ (Y /\ Z)) by Th28
.= X \/ ((X \/ Y) /\ Z) by Th32
.= ((X \/ Y) /\ X) \/ ((X \/ Y) /\ Z) by Th30
.= (X \/ Y) /\ (X \/ Z) by Th32 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st (X /\ Y) \/ (X /\ Z) = X holds
X c= Y \/ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z )
assume  (X /\ Y) \/ (X /\ Z) = X ; ::_thesis: X c= Y \/ Z
then  X = X /\ (Y \/ Z) by Th32;
hence  X c= Y \/ Z by Th15; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st (X \/ Y) /\ (X \/ Z) = X holds
Y /\ Z c= X
let X, Y, Z be ManySortedSet of I; ::_thesis: ( (X \/ Y) /\ (X \/ Z) = X implies Y /\ Z c= X )
assume  (X \/ Y) /\ (X \/ Z) = X ; ::_thesis: Y /\ Z c= X
then  X = X \/ (Y /\ Z) by Th33;
hence  Y /\ Z c= X by Th14; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
let X, Y, Z be ManySortedSet of I; ::_thesis: ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
thus ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = (((X /\ Y) \/ (Y /\ Z)) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th33
.= ((X /\ Y) \/ ((Y /\ Z) \/ Z)) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th28
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th31
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ X) \/ (Y /\ Z)) by Th28
.= ((X /\ Y) \/ Z) /\ (X \/ (Y /\ Z)) by Th31
.= ((X \/ Z) /\ (Y \/ Z)) /\ (X \/ (Y /\ Z)) by Th33
.= ((X \/ Z) /\ (Y \/ Z)) /\ ((X \/ Y) /\ (X \/ Z)) by Th33
.= (X \/ Y) /\ (((Y \/ Z) /\ (X \/ Z)) /\ (X \/ Z)) by Th29
.= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th29
.= ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X) by Th29 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X \/ Y c= Z holds
X c= Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X \/ Y c= Z implies X c= Z )
 X c= X \/ Y by Th14;
hence  ( X \/ Y c= Z implies X c= Z ) by Th13; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y /\ Z holds
X c= Y
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y /\ Z implies X c= Y )
 Y /\ Z c= Y by Th15;
hence  ( X c= Y /\ Z implies X c= Y ) by Th13; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
thus (X \/ Y) \/ Z = X \/ (Y \/ (Z \/ Z)) by Th28
.= X \/ ((Z \/ Y) \/ Z) by Th28
.= (X \/ Z) \/ (Y \/ Z) by Th28 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X /\ Y) /\ Z = (X /\ Z) /\ (Y /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X /\ Y) /\ Z = (X /\ Z) /\ (Y /\ Z)
thus (X /\ Y) /\ Z = X /\ (Y /\ (Z /\ Z)) by Th29
.= X /\ ((Z /\ Y) /\ Z) by Th29
.= (X /\ Z) /\ (Y /\ Z) by Th29 ; ::_thesis: verum
end;

theorem :: PBOOLE:41
for I being set
for X, Y being ManySortedSet of I holds X \/ (X \/ Y) = X \/ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ (X \/ Y) = X \/ Y
let X, Y be ManySortedSet of I; ::_thesis: X \/ (X \/ Y) = X \/ Y
thus X \/ (X \/ Y) = (X \/ X) \/ Y by Th28
.= X \/ Y ; ::_thesis: verum
end;

theorem :: PBOOLE:42
for I being set
for X, Y being ManySortedSet of I holds X /\ (X /\ Y) = X /\ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ (X /\ Y) = X /\ Y
let X, Y be ManySortedSet of I; ::_thesis: X /\ (X /\ Y) = X /\ Y
thus X /\ (X /\ Y) = (X /\ X) /\ Y by Th29
.= X /\ Y ; ::_thesis: verum
end;

begin

theorem Th43: :: PBOOLE:43
for I being set
for X being ManySortedSet of I holds [[0]] I c= X
proof
let I be set ; ::_thesis: for X being ManySortedSet of I holds [[0]] I c= X
let X be ManySortedSet of I; ::_thesis: [[0]] I c= X
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies ([[0]] I) . i c= X . i )
assume A1: i in I ; ::_thesis: ([[0]] I) . i c= X . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ([[0]] I) . i or e in X . i )
assume  e in ([[0]] I) . i ; ::_thesis: e in X . i
hence  e in X . i by A1, FUNCOP_1:7; ::_thesis: verum
end;

theorem Th44: :: PBOOLE:44
for I being set
for X being ManySortedSet of I st X c= [[0]] I holds
X = [[0]] I
proof
let I be set ; ::_thesis: for X being ManySortedSet of I st X c= [[0]] I holds
X = [[0]] I
let X be ManySortedSet of I; ::_thesis: ( X c= [[0]] I implies X = [[0]] I )
assume  X c= [[0]] I ; ::_thesis: X = [[0]] I
then  ( X c= [[0]] I & [[0]] I c= X ) by Th43;
hence  X = [[0]] I by Lm1; ::_thesis: verum
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 = [[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 & 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 & ([[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 & X /\ Z = [[0]] I holds
X c= Y
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y \/ Z & X /\ Z = [[0]] I holds
X c= Y
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y \/ Z & X /\ Z = [[0]] I implies X c= Y )
assume that
A1: X c= Y \/ Z and
A2: X /\ Z = [[0]] I ; ::_thesis: X c= Y
 X /\ (Y \/ Z) = X by A1, Th23;
then  (Y /\ X) \/ ([[0]] I) = X by A2, Th32;
then  Y /\ X = X by Th22, Th43;
hence  X c= Y by Th15; ::_thesis: verum
end;

theorem :: PBOOLE:51
for I being set
for Y, X being ManySortedSet of I st Y c= X & 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 )
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds
( X \ Y = [[0]] I iff X c= Y )
let X, Y be ManySortedSet of I; ::_thesis: ( X \ Y = [[0]] I iff X c= Y )
hereby  ::_thesis: ( X c= Y implies X \ Y = [[0]] I )
assume A1: X \ Y = [[0]] I ; ::_thesis: X c= Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_c=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i c= Y . i )
assume  i in I ; ::_thesis: X . i c= Y . i
then (X . i) \ (Y . i) = (X \ Y) . i by Def6
.= {} by A1, Th5 ;
hence  X . i c= Y . i by XBOOLE_1:37; ::_thesis: verum
end;
hence  X c= Y by Def2; ::_thesis: verum
end;
assume A2: X c= Y ; ::_thesis: X \ Y = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(X_\_Y)_._i_=_{}
let i be set ; ::_thesis: ( i in I implies (X \ Y) . i = {} )
assume A3: i in I ; ::_thesis: (X \ Y) . i = {}
then A4: X . i c= Y . i by A2, Def2;
thus (X \ Y) . i = (X . i) \ (Y . i) by A3, Def6
.= {} by A4, XBOOLE_1:37 ; ::_thesis: verum
end;
hence  X \ Y = [[0]] I by Th6; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
X \ Z c= Y \ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y implies X \ Z c= Y \ Z )
assume A1: X c= Y ; ::_thesis: X \ Z c= Y \ Z
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(X_\_Z)_._i_c=_(Y_\_Z)_._i
let i be set ; ::_thesis: ( i in I implies (X \ Z) . i c= (Y \ Z) . i )
assume A2: i in I ; ::_thesis: (X \ Z) . i c= (Y \ Z) . i
then A3: ( (X \ Z) . i = (X . i) \ (Z . i) & (Y \ Z) . i = (Y . i) \ (Z . i) ) by Def6;
 X . i c= Y . i by A1, A2, Def2;
hence  (X \ Z) . i c= (Y \ Z) . i by A3, XBOOLE_1:33; ::_thesis: verum
end;
hence  X \ Z c= Y \ Z by Def2; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
Z \ Y c= Z \ X
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y implies Z \ Y c= Z \ X )
assume A1: X c= Y ; ::_thesis: Z \ Y c= Z \ X
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(Z_\_Y)_._i_c=_(Z_\_X)_._i
let i be set ; ::_thesis: ( i in I implies (Z \ Y) . i c= (Z \ X) . i )
assume A2: i in I ; ::_thesis: (Z \ Y) . i c= (Z \ X) . i
then A3: ( (Z \ X) . i = (Z . i) \ (X . i) & (Z \ Y) . i = (Z . i) \ (Y . i) ) by Def6;
 X . i c= Y . i by A1, A2, Def2;
hence  (Z \ Y) . i c= (Z \ X) . i by A3, XBOOLE_1:34; ::_thesis: verum
end;
hence  Z \ Y c= Z \ X by Def2; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \ V c= Y \ Z
let X, Y, Z, V be ManySortedSet of I; ::_thesis: ( X c= Y & Z c= V implies X \ V c= Y \ Z )
assume  ( X c= Y & Z c= V ) ; ::_thesis: X \ V c= Y \ Z
then  ( X \ V c= Y \ V & Y \ V c= Y \ Z ) by Th53, Th54;
hence  X \ V c= Y \ Z by Th13; ::_thesis: verum
end;

theorem Th56: :: PBOOLE:56
for I being set
for X, Y being ManySortedSet of I holds X \ Y c= X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ Y c= X
let X, Y be ManySortedSet of I; ::_thesis: X \ Y c= X
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(X_\_Y)_._i_c=_X_._i
let i be set ; ::_thesis: ( i in I implies (X \ Y) . i c= X . i )
assume A1: i in I ; ::_thesis: (X \ Y) . i c= X . i
 (X . i) \ (Y . i) c= X . i ;
hence  (X \ Y) . i c= X . i by A1, Def6; ::_thesis: verum
end;
hence  X \ Y c= X by Def2; ::_thesis: verum
end;

theorem :: PBOOLE:57
for I being set
for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [[0]] I
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y \ X holds
X = [[0]] I
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y \ X implies X = [[0]] I )
assume A1: X c= Y \ X ; ::_thesis: X = [[0]] I
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies X . i = ([[0]] I) . i )
assume A2: i in I ; ::_thesis: X . i = ([[0]] I) . i
then  X . i c= (Y \ X) . i by A1, Def2;
then  X . i c= (Y . i) \ (X . i) by A2, Def6;
hence X . i = {} by XBOOLE_1:38
.= ([[0]] I) . i by Th5 ;
::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for X being ManySortedSet of I holds X \ ([[0]] I) = X
let X be ManySortedSet of I; ::_thesis: X \ ([[0]] I) = X
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X \ ([[0]] I)) . i = X . i )
assume  i in I ; ::_thesis: (X \ ([[0]] I)) . i = X . i
hence (X \ ([[0]] I)) . i = (X . i) \ (([[0]] I) . i) by Def6
.= (X . i) \ {} by Th5
.= X . i ;
::_thesis: verum
end;

theorem Th60: :: PBOOLE:60
for I being set
for X being ManySortedSet of I holds ([[0]] I) \ X = [[0]] I
proof
let I be set ; ::_thesis: for X being ManySortedSet of I holds ([[0]] I) \ X = [[0]] I
let X be ManySortedSet of I; ::_thesis: ([[0]] I) \ X = [[0]] I
 [[0]] I c= X by Th43;
hence  ([[0]] I) \ X = [[0]] I by Th52; ::_thesis: verum
end;

theorem :: PBOOLE:61
for I being set
for X, Y being ManySortedSet of I holds X \ (X \/ Y) = [[0]] I
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ (X \/ Y) = [[0]] I
let X, Y be ManySortedSet of I; ::_thesis: X \ (X \/ Y) = [[0]] I
 X c= X \/ Y by Th14;
hence  X \ (X \/ Y) = [[0]] I by Th52; ::_thesis: verum
end;

theorem Th62: :: PBOOLE:62
for I being set
for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ Z
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: X /\ (Y \ Z) = (X /\ Y) \ Z
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X /\ (Y \ Z)) . i = ((X /\ Y) \ Z) . i )
assume A1: i in I ; ::_thesis: (X /\ (Y \ Z)) . i = ((X /\ Y) \ Z) . i
hence (X /\ (Y \ Z)) . i = (X . i) /\ ((Y \ Z) . i) by Def5
.= (X . i) /\ ((Y . i) \ (Z . i)) by A1, Def6
.= ((X . i) /\ (Y . i)) \ (Z . i) by XBOOLE_1:49
.= ((X /\ Y) . i) \ (Z . i) by A1, Def5
.= ((X /\ Y) \ Z) . i by A1, Def6 ;
::_thesis: verum
end;

theorem Th63: :: PBOOLE:63
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) /\ Y = [[0]] I
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds (X \ Y) /\ Y = [[0]] I
let X, Y be ManySortedSet of I; ::_thesis: (X \ Y) /\ Y = [[0]] I
A1: Y /\ X c= Y by Th15;
thus (X \ Y) /\ Y = (Y /\ X) \ Y by Th62
.= [[0]] I by A1, Th52 ; ::_thesis: verum
thus  verum ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X \ (Y \ Z)) . i = ((X \ Y) \/ (X /\ Z)) . i )
assume A1: i in I ; ::_thesis: (X \ (Y \ Z)) . i = ((X \ Y) \/ (X /\ Z)) . i
hence (X \ (Y \ Z)) . i = (X . i) \ ((Y \ Z) . i) by Def6
.= (X . i) \ ((Y . i) \ (Z . i)) by A1, Def6
.= ((X . i) \ (Y . i)) \/ ((X . i) /\ (Z . i)) by XBOOLE_1:52
.= ((X . i) \ (Y . i)) \/ ((X /\ Z) . i) by A1, Def5
.= ((X \ Y) . i) \/ ((X /\ Z) . i) by A1, Def6
.= ((X \ Y) \/ (X /\ Z)) . i by A1, Def4 ;
::_thesis: verum
end;

theorem Th65: :: PBOOLE:65
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \/ (X /\ Y) = X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds (X \ Y) \/ (X /\ Y) = X
let X, Y be ManySortedSet of I; ::_thesis: (X \ Y) \/ (X /\ Y) = X
thus (X \ Y) \/ (X /\ Y) = X \ (Y \ Y) by Th64
.= X \ ([[0]] I) by Th52
.= X by Th59 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y holds
Y = X \/ (Y \ X)
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y implies Y = X \/ (Y \ X) )
assume A1: X c= Y ; ::_thesis: Y = X \/ (Y \ X)
thus Y = (Y \ X) \/ (Y /\ X) by Th65
.= X \/ (Y \ X) by A1, Th23 ; ::_thesis: verum
end;

theorem Th67: :: PBOOLE:67
for I being set
for X, Y being ManySortedSet of I holds X \/ (Y \ X) = X \/ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ (Y \ X) = X \/ Y
let X, Y be ManySortedSet of I; ::_thesis: X \/ (Y \ X) = X \/ Y
thus X \/ (Y \ X) = (X \/ (Y /\ X)) \/ (Y \ X) by Th31
.= X \/ ((Y /\ X) \/ (Y \ X)) by Th28
.= X \/ Y by Th65 ; ::_thesis: verum
end;

theorem Th68: :: PBOOLE:68
for I being set
for X, Y being ManySortedSet of I holds X \ (X \ Y) = X /\ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ (X \ Y) = X /\ Y
let X, Y be ManySortedSet of I; ::_thesis: X \ (X \ Y) = X /\ Y
thus X \ (X \ Y) = (X \ X) \/ (X /\ Y) by Th64
.= ([[0]] I) \/ (X /\ Y) by Th52
.= X /\ Y by Th22, Th43 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X \ (Y /\ Z)) . i = ((X \ Y) \/ (X \ Z)) . i )
assume A1: i in I ; ::_thesis: (X \ (Y /\ Z)) . i = ((X \ Y) \/ (X \ Z)) . i
hence (X \ (Y /\ Z)) . i = (X . i) \ ((Y /\ Z) . i) by Def6
.= (X . i) \ ((Y . i) /\ (Z . i)) by A1, Def5
.= ((X . i) \ (Y . i)) \/ ((X . i) \ (Z . i)) by XBOOLE_1:54
.= ((X . i) \ (Y . i)) \/ ((X \ Z) . i) by A1, Def6
.= ((X \ Y) . i) \/ ((X \ Z) . i) by A1, Def6
.= ((X \ Y) \/ (X \ Z)) . i by A1, Def4 ;
::_thesis: verum
end;

theorem Th70: :: PBOOLE:70
for I being set
for X, Y being ManySortedSet of I holds X \ (X /\ Y) = X \ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ (X /\ Y) = X \ Y
let X, Y be ManySortedSet of I; ::_thesis: X \ (X /\ Y) = X \ Y
thus X \ (X /\ Y) = (X \ X) \/ (X \ Y) by Th69
.= ([[0]] I) \/ (X \ Y) by Th52
.= X \ Y by Th22, Th43 ; ::_thesis: verum
end;

theorem :: PBOOLE:71
for I being set
for X, Y being ManySortedSet of I holds
( X /\ Y = [[0]] I iff X \ Y = X )
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds
( X /\ Y = [[0]] I iff X \ Y = X )
let X, Y be ManySortedSet of I; ::_thesis: ( X /\ Y = [[0]] I iff X \ Y = X )
hereby  ::_thesis: ( X \ Y = X implies X /\ Y = [[0]] I )
assume A1: X /\ Y = [[0]] I ; ::_thesis: X \ Y = X
thus X \ Y = X \ (X /\ Y) by Th70
.= X by A1, Th59 ; ::_thesis: verum
end;
thus  ( X \ Y = X implies X /\ Y = [[0]] I ) by Th63; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies ((X \/ Y) \ Z) . i = ((X \ Z) \/ (Y \ Z)) . i )
assume A1: i in I ; ::_thesis: ((X \/ Y) \ Z) . i = ((X \ Z) \/ (Y \ Z)) . i
hence ((X \/ Y) \ Z) . i = ((X \/ Y) . i) \ (Z . i) by Def6
.= ((X . i) \/ (Y . i)) \ (Z . i) by A1, Def4
.= ((X . i) \ (Z . i)) \/ ((Y . i) \ (Z . i)) by XBOOLE_1:42
.= ((X . i) \ (Z . i)) \/ ((Y \ Z) . i) by A1, Def6
.= ((X \ Z) . i) \/ ((Y \ Z) . i) by A1, Def6
.= ((X \ Z) \/ (Y \ Z)) . i by A1, Def4 ;
::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \ Y) \ Z = X \ (Y \/ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \ Y) \ Z = X \ (Y \/ Z)
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies ((X \ Y) \ Z) . i = (X \ (Y \/ Z)) . i )
assume A1: i in I ; ::_thesis: ((X \ Y) \ Z) . i = (X \ (Y \/ Z)) . i
hence ((X \ Y) \ Z) . i = ((X \ Y) . i) \ (Z . i) by Def6
.= ((X . i) \ (Y . i)) \ (Z . i) by A1, Def6
.= (X . i) \ ((Y . i) \/ (Z . i)) by XBOOLE_1:41
.= (X . i) \ ((Y \/ Z) . i) by A1, Def4
.= (X \ (Y \/ Z)) . i by A1, Def6 ;
::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z)
A1: X \ Z c= X by Th56;
thus (X /\ Y) \ Z = (X \ Z) /\ Y by Th62
.= (X \ Z) \ ((X \ Z) \ Y) by Th68
.= (X \ Z) \ (X \ (Z \/ Y)) by Th73
.= ((X \ Z) \ X) \/ ((X \ Z) /\ (Z \/ Y)) by Th64
.= ([[0]] I) \/ ((X \ Z) /\ (Z \/ Y)) by A1, Th52
.= (X \ Z) /\ (Y \/ Z) by Th22, Th43
.= (X \ Z) /\ ((Y \ Z) \/ Z) by Th67
.= ((X \ Z) /\ (Y \ Z)) \/ ((X \ Z) /\ Z) by Th32
.= ((X \ Z) /\ (Y \ Z)) \/ ([[0]] I) by Th63
.= (X \ Z) /\ (Y \ Z) by Th22, Th43 ; ::_thesis: verum
end;

theorem Th75: :: PBOOLE:75
for I being set
for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y
let X, Y be ManySortedSet of I; ::_thesis: (X \/ Y) \ Y = X \ Y
thus (X \/ Y) \ Y = (X \ Y) \/ (Y \ Y) by Th72
.= (X \ Y) \/ ([[0]] I) by Th52
.= X \ Y by Th22, Th43 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y \/ Z holds
( X \ Y c= Z & X \ Z c= Y )
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y \/ Z implies ( X \ Y c= Z & X \ Z c= Y ) )
assume A1: X c= Y \/ Z ; ::_thesis: ( X \ Y c= Z & X \ Z c= Y )
then  X \ Y c= (Z \/ Y) \ Y by Th53;
then A2: X \ Y c= Z \ Y by Th75;
 Z \ Y c= Z by Th56;
hence  X \ Y c= Z by A2, Th13; ::_thesis: X \ Z c= Y
 X \ Z c= (Y \/ Z) \ Z by A1, Th53;
then A3: X \ Z c= Y \ Z by Th75;
 Y \ Z c= Y by Th56;
hence  X \ Z c= Y by A3, Th13; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
let X, Y be ManySortedSet of I; ::_thesis: (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
thus (X \/ Y) \ (X /\ Y) = (X \ (X /\ Y)) \/ (Y \ (X /\ Y)) by Th72
.= (X \ Y) \/ (Y \ (X /\ Y)) by Th70
.= (X \ Y) \/ (Y \ X) by Th70 ; ::_thesis: verum
end;

theorem Th78: :: PBOOLE:78
for I being set
for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y
let X, Y be ManySortedSet of I; ::_thesis: (X \ Y) \ Y = X \ Y
thus (X \ Y) \ Y = X \ (Y \/ Y) by Th73
.= X \ Y ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
thus X \ (Y \/ Z) = (X \ Y) \ Z by Th73
.= ((X \ Y) /\ X) \ Z by Th56, Th23
.= (X \ Y) /\ (X \ Z) by Th62 ; ::_thesis: verum
end;

theorem :: PBOOLE:80
for I being set
for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y
let X, Y be ManySortedSet of I; ::_thesis: ( X \ Y = Y \ X implies X = Y )
assume  X \ Y = Y \ X ; ::_thesis: X = Y
hence X = (Y \ X) \/ (Y /\ X) by Th65
.= Y by Th65 ;
::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
A1: X /\ Y c= X by Th15;
(X /\ Y) \ (X /\ Z) = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Th69
.= ([[0]] I) \/ ((X /\ Y) \ Z) by A1, Th52
.= (X /\ Y) \ Z by Th22, Th43 ;
hence  X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th62; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X \ Y c= Z holds
X c= Y \/ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X \ Y c= Z implies X c= Y \/ Z )
assume A1: X \ Y c= Z ; ::_thesis: X c= Y \/ Z
 X /\ Y c= Y by Th15;
then  (X /\ Y) \/ (X \ Y) c= Y \/ Z by A1, Th20;
hence  X c= Y \/ Z by Th65; ::_thesis: verum
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 \+\ ([[0]] I) = X
proof
let I be set ; ::_thesis: for X being ManySortedSet of I holds X \+\ ([[0]] I) = X
let X be ManySortedSet of I; ::_thesis: X \+\ ([[0]] I) = X
thus X \+\ ([[0]] I) = X \/ (([[0]] I) \ X) by Th59
.= X \/ ([[0]] I) by Th60
.= X by Th22, Th43 ; ::_thesis: verum
end;

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)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \/ (X /\ Y)
let X, Y be ManySortedSet of I; ::_thesis: X \/ Y = (X \+\ Y) \/ (X /\ Y)
thus X \/ Y = ((X \ Y) \/ (X /\ Y)) \/ Y by Th65
.= (X \ Y) \/ ((X /\ Y) \/ Y) by Th28
.= (X \ Y) \/ Y by Th31
.= (X \ Y) \/ ((Y \ X) \/ (Y /\ X)) by Th65
.= (X \+\ Y) \/ (X /\ Y) by Th28 ; ::_thesis: verum
end;

theorem Th87: :: PBOOLE:87
for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \/ Y) \ (X /\ Y)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \+\ Y = (X \/ Y) \ (X /\ Y)
let X, Y be ManySortedSet of I; ::_thesis: X \+\ Y = (X \/ Y) \ (X /\ Y)
thus X \+\ Y = (X \ (X /\ Y)) \/ (Y \ X) by Th70
.= (X \ (X /\ Y)) \/ (Y \ (X /\ Y)) by Th70
.= (X \/ Y) \ (X /\ Y) by Th72 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
thus (X \+\ Y) \ Z = ((X \ Y) \ Z) \/ ((Y \ X) \ Z) by Th72
.= (X \ (Y \/ Z)) \/ ((Y \ X) \ Z) by Th73
.= (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)) by Th73 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)
thus X \ (Y \+\ Z) = X \ ((Y \/ Z) \ (Y /\ Z)) by Th87
.= (X \ (Y \/ Z)) \/ (X /\ (Y /\ Z)) by Th64
.= (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z) by Th29 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
let X, Y, Z be ManySortedSet of I; ::_thesis: (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
set S1 = X \ (Y \/ Z);
set S2 = Y \ (X \/ Z);
set S3 = Z \ (X \/ Y);
set S4 = (X /\ Y) /\ Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th72
.= ((X \ (Y \/ Z)) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th73
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th73
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th77
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (((X /\ Y) /\ Z) \/ (Z \ (X \/ Y))) by Th64
.= (((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ ((X /\ Y) /\ Z)) \/ (Z \ (X \/ Y)) by Th28
.= (((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ (X \/ Y)) by Th28
.= ((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th28
.= ((X \ (Y \/ Z)) \/ (X /\ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th29
.= (X \ ((Y \/ Z) \ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th64
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (X \/ Z)) \/ (Z \ (Y \/ X))) by Th77
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (Z \/ X)) \/ ((Z \ Y) \ X)) by Th73
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ (((Y \ Z) \ X) \/ ((Z \ Y) \ X)) by Th73
.= X \+\ (Y \+\ Z) by Th72 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ Y = X \+\ (Y \ X)
let X, Y be ManySortedSet of I; ::_thesis: X \/ Y = X \+\ (Y \ X)
thus X \/ Y = Y \/ (X \/ X)
.= (X \/ Y) \/ X by Th28
.= ((X \ Y) \/ Y) \/ X by Th67
.= (X \ Y) \/ (X \/ Y) by Th28
.= (X \ Y) \/ (X \/ (Y \ X)) by Th67
.= ((X \ Y) \/ (X /\ X)) \/ (Y \ X) by Th28
.= (X \ (Y \ X)) \/ (Y \ X) by Th64
.= X \+\ (Y \ X) by Th78 ; ::_thesis: verum
end;

theorem Th93: :: PBOOLE:93
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = X \+\ (X \ Y)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ Y = X \+\ (X \ Y)
let X, Y be ManySortedSet of I; ::_thesis: X /\ Y = X \+\ (X \ Y)
A1: X \ Y c= X by Th56;
thus X /\ Y = X \ (X \ Y) by Th68
.= (X \ (X \ Y)) \/ ([[0]] I) by Th22, Th43
.= X \+\ (X \ Y) by A1, Th52 ; ::_thesis: verum
end;

theorem Th94: :: PBOOLE:94
for I being set
for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ Y = X \+\ (X /\ Y)
let X, Y be ManySortedSet of I; ::_thesis: X \ Y = X \+\ (X /\ Y)
A1: X /\ Y c= X by Th15;
thus X \ Y = X \ (X /\ Y) by Th70
.= (X \ (X /\ Y)) \/ ([[0]] I) by Th22, Th43
.= X \+\ (X /\ Y) by A1, Th52 ; ::_thesis: verum
end;

theorem Th95: :: PBOOLE:95
for I being set
for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)
proof
let I be set ; ::_thesis: for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)
let Y, X be ManySortedSet of I; ::_thesis: Y \ X = X \+\ (X \/ Y)
A1: X c= Y \/ X by Th14;
thus Y \ X = (Y \/ X) \ X by Th75
.= ([[0]] I) \/ ((Y \/ X) \ X) by Th22, Th43
.= X \+\ (X \/ Y) by A1, Th52 ; ::_thesis: verum
end;

theorem :: PBOOLE:96
for I being set
for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
let X, Y be ManySortedSet of I; ::_thesis: X \/ Y = (X \+\ Y) \+\ (X /\ Y)
thus X \/ Y = X \+\ (Y \ X) by Th92
.= X \+\ (Y \+\ (X /\ Y)) by Th94
.= (X \+\ Y) \+\ (X /\ Y) by Th90 ; ::_thesis: verum
end;

theorem :: PBOOLE:97
for I being set
for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
let X, Y be ManySortedSet of I; ::_thesis: X /\ Y = (X \+\ Y) \+\ (X \/ Y)
thus X /\ Y = X \+\ (X \ Y) by Th93
.= X \+\ (Y \+\ (X \/ Y)) by Th95
.= (X \+\ Y) \+\ (X \/ Y) by Th90 ; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st ( X overlaps Y or X overlaps Z ) holds
X overlaps Y \/ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( ( X overlaps Y or X overlaps Z ) implies X overlaps Y \/ Z )
assume A1: ( X overlaps Y or X overlaps Z ) ; ::_thesis: X overlaps Y \/ Z
percases ( X overlaps Y or X overlaps Z ) by A1;
suppose X overlaps Y ; ::_thesis: X overlaps Y \/ Z
then consider x being ManySortedSet of I such that
A2: x in X and
A3: x in Y by Th11;
 x in Y \/ Z by A3, Th7;
hence  X overlaps Y \/ Z by A2, Th10; ::_thesis: verum
end;
suppose X overlaps Z ; ::_thesis: X overlaps Y \/ Z
then consider x being ManySortedSet of I such that
A4: x in X and
A5: x in Z by Th11;
 x in Y \/ Z by A5, Th7;
hence  X overlaps Y \/ Z by A4, Th10; ::_thesis: verum
end;
end;
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X overlaps Y & Y c= Z holds
X overlaps Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X overlaps Y & Y c= Z implies X overlaps Z )
assume that
A1: X overlaps Y and
A2: Y c= Z ; ::_thesis: X overlaps Z
consider x being ManySortedSet of I such that
A3: x in X and
A4: x in Y by A1, Th11;
 x in Z by A2, A4, Th9;
hence  X overlaps Z by A3, Th10; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X overlaps Y & X c= Z holds
Z overlaps Y
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X overlaps Y & X c= Z implies Z overlaps Y )
assume that
A1: X overlaps Y and
A2: X c= Z ; ::_thesis: Z overlaps Y
consider x being ManySortedSet of I such that
A3: x in X and
A4: x in Y by A1, Th11;
 x in Z by A2, A3, Th9;
hence  Z overlaps Y by A4, Th10; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V & X overlaps Z holds
Y overlaps V
let X, Y, Z, V be ManySortedSet of I; ::_thesis: ( X c= Y & Z c= V & X overlaps Z implies Y overlaps V )
assume that
A1: X c= Y and
A2: Z c= V ; ::_thesis: ( not X overlaps Z or Y overlaps V )
assume  X overlaps Z ; ::_thesis: Y overlaps V
then  Y overlaps Z by A1, Th100;
hence  Y overlaps V by A2, Th99; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X overlaps Y /\ Z holds
( X overlaps Y & X overlaps Z )
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X overlaps Y /\ Z implies ( X overlaps Y & X overlaps Z ) )
assume  X overlaps Y /\ Z ; ::_thesis: ( X overlaps Y & X overlaps Z )
then consider x being ManySortedSet of I such that
A1: x in X and
A2: x in Y /\ Z by Th11;
 ( x in Y & x in Z ) by A2, Th8;
hence  ( X overlaps Y & X overlaps Z ) by A1, Th10; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Z, V being ManySortedSet of I st X overlaps Z & X c= V holds
X overlaps Z /\ V
let X, Z, V be ManySortedSet of I; ::_thesis: ( X overlaps Z & X c= V implies X overlaps Z /\ V )
assume that
A1: X overlaps Z and
A2: X c= V ; ::_thesis: X overlaps Z /\ V
consider x being ManySortedSet of I such that
A3: x in X and
A4: x in Z by A1, Th11;
 x in V by A2, A3, Th9;
then  x in Z /\ V by A4, Th8;
hence  X overlaps Z /\ V by A3, Th10; ::_thesis: verum
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 Y, Z, X being ManySortedSet of I st not Y overlaps Z holds
not X /\ Y overlaps X /\ Z
proof
let I be set ; ::_thesis: for Y, Z, X being ManySortedSet of I st not Y overlaps Z holds
not X /\ Y overlaps X /\ Z
let Y, Z, X be ManySortedSet of I; ::_thesis: ( not Y overlaps Z implies not X /\ Y overlaps X /\ Z )
assume A1: not Y overlaps Z ; ::_thesis: not X /\ Y overlaps X /\ Z
 ( X /\ Y c= Y & X /\ Z c= Z ) by Th15;
hence  not X /\ Y overlaps X /\ Z by A1, Th101; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
Y overlaps X \ Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X overlaps Y \ Z implies Y overlaps X \ Z )
assume A1: X overlaps Y \ Z ; ::_thesis: Y overlaps X \ Z
let i be set ; :: according to PBOOLE:def_7 ::_thesis: ( i in I implies Y . i meets (X \ Z) . i )
assume A2: i in I ; ::_thesis: Y . i meets (X \ Z) . i
then  X . i meets (Y \ Z) . i by A1, Def7;
then  X . i meets (Y . i) \ (Z . i) by A2, Def6;
then  Y . i meets (X . i) \ (Z . i) by XBOOLE_1:81;
hence  Y . i meets (X \ Z) . i by A2, Def6; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X meets Y & Y c= Z holds
X meets Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X meets Y & Y c= Z implies X meets Z )
assume that
A1: X meets Y and
A2: Y c= Z ; ::_thesis: X meets Z
consider i being set  such that
A3: i in I and
A4: X . i meets Y . i by A1, Def8;
take  i ; :: according to PBOOLE:def_8 ::_thesis: ( i in I & not X . i misses Z . i )
 Y . i c= Z . i by A2, A3, Def2;
hence  ( i in I & not X . i misses Z . i ) by A3, A4, XBOOLE_1:63; ::_thesis: verum
end;

theorem Th108: :: PBOOLE:108
for I being set
for Y, X being ManySortedSet of I holds Y misses X \ Y
proof
let I be set ; ::_thesis: for Y, X being ManySortedSet of I holds Y misses X \ Y
let Y, X be ManySortedSet of I; ::_thesis: Y misses X \ Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
Y_._i_misses_(X_\_Y)_._i
let i be set ; ::_thesis: ( i in I implies Y . i misses (X \ Y) . i )
assume  i in I ; ::_thesis: Y . i misses (X \ Y) . i
then  (X \ Y) . i = (X . i) \ (Y . i) by Def6;
hence  Y . i misses (X \ Y) . i by XBOOLE_1:79; ::_thesis: verum
end;
hence  Y misses X \ Y by Def8; ::_thesis: verum
end;

theorem :: PBOOLE:109
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y
let X, Y be ManySortedSet of I; ::_thesis: X /\ Y misses X \ Y
 ( X /\ Y c= Y & X \ Y misses Y ) by Th15, Th108;
hence  X /\ Y misses X \ Y by Th107; ::_thesis: verum
end;

theorem :: PBOOLE:110
for I being set
for X, Y being ManySortedSet of I holds X /\ Y misses X \+\ Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X /\ Y misses X \+\ Y
let X, Y be ManySortedSet of I; ::_thesis: X /\ Y misses X \+\ Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(X_/\_Y)_._i_misses_(X_\+\_Y)_._i
let i be set ; ::_thesis: ( i in I implies (X /\ Y) . i misses (X \+\ Y) . i )
assume  i in I ; ::_thesis: (X /\ Y) . i misses (X \+\ Y) . i
then  ( (X /\ Y) . i = (X . i) /\ (Y . i) & (X \+\ Y) . i = (X . i) \+\ (Y . i) ) by Def5, Th4;
hence  (X /\ Y) . i misses (X \+\ Y) . i by XBOOLE_1:103; ::_thesis: verum
end;
hence  X /\ Y misses X \+\ Y by Def8; ::_thesis: verum
end;

theorem Th111: :: PBOOLE:111
for I being set
for X, Y being ManySortedSet of I st X misses Y holds
X /\ Y = [[0]] I
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X misses Y holds
X /\ Y = [[0]] I
let X, Y be ManySortedSet of I; ::_thesis: ( X misses Y implies X /\ Y = [[0]] I )
assume A1: X misses Y ; ::_thesis: X /\ Y = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(X_/\_Y)_._i_=_{}
let i be set ; ::_thesis: ( i in I implies (X /\ Y) . i = {} )
assume A2: i in I ; ::_thesis: (X /\ Y) . i = {}
then A3: X . i misses Y . i by A1, Def8;
thus (X /\ Y) . i = (X . i) /\ (Y . i) by A2, Def5
.= {} by A3, XBOOLE_0:def_7 ; ::_thesis: verum
end;
hence  X /\ Y = [[0]] I by Th6; ::_thesis: verum
end;

theorem :: PBOOLE:112
for I being set
for X being ManySortedSet of I st X <> [[0]] I holds
X meets X
proof
let I be set ; ::_thesis: for X being ManySortedSet of I st X <> [[0]] I holds
X meets X
let X be ManySortedSet of I; ::_thesis: ( X <> [[0]] I implies X meets X )
 X = X /\ X ;
hence  ( X <> [[0]] I implies X meets X ) by Th111; ::_thesis: verum
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 = [[0]] I
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y misses Z holds
X = [[0]] I
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X c= Y & X c= Z & Y misses Z implies X = [[0]] I )
assume A1: ( X c= Y & X c= Z ) ; ::_thesis: ( not Y misses Z or X = [[0]] I )
assume  Y misses Z ; ::_thesis: X = [[0]] I
then  Y /\ Z = [[0]] I by Th111;
hence  X = [[0]] I by A1, Th17, Th44; ::_thesis: verum
end;

theorem :: PBOOLE:114
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
let I be set ; ::_thesis: 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 )
let Z, V, X, Y be ManySortedSet of I; ::_thesis: ( Z \/ V = X \/ Y & X misses Z & Y misses V implies ( X = V & Y = Z ) )
assume A1: Z \/ V = X \/ Y ; ::_thesis: ( not X misses Z or not Y misses V or ( X = V & Y = Z ) )
assume  ( X misses Z & Y misses V ) ; ::_thesis: ( X = V & Y = Z )
then A2: ( X /\ Z = [[0]] I & Y /\ V = [[0]] I ) by Th111;
thus X = X /\ (Z \/ V) by Th23, A1, Th14
.= (X /\ Z) \/ (X /\ V) by Th32
.= (X \/ Y) /\ V by A2, Th32
.= V by A1, Th14, Th23 ; ::_thesis: Y = Z
thus Y = Y /\ (Z \/ V) by Th23, A1, Th14
.= (Y /\ Z) \/ (Y /\ V) by Th32
.= (X \/ Y) /\ Z by A2, Th32
.= Z by A1, Th14, Th23 ; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X misses Y holds
X \ Y = X
let X, Y be ManySortedSet of I; ::_thesis: ( X misses Y implies X \ Y = X )
assume A1: X misses Y ; ::_thesis: X \ Y = X
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( i in I implies (X \ Y) . i = X . i )
assume A2: i in I ; ::_thesis: (X \ Y) . i = X . i
then A3: (X \ Y) . i = (X . i) \ (Y . i) by Def6;
 X . i misses Y . i by A1, A2, Def8;
hence  (X \ Y) . i = X . i by A3, XBOOLE_1:83; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X misses Y holds
(X \/ Y) \ Y = X
let X, Y be ManySortedSet of I; ::_thesis: ( X misses Y implies (X \/ Y) \ Y = X )
 (X \/ Y) \ Y = X \ Y by Th75;
hence  ( X misses Y implies (X \/ Y) \ Y = X ) by Th115; ::_thesis: verum
end;

theorem :: PBOOLE:117
for I being set
for X, Y being ManySortedSet of I st X \ Y = X holds
X misses Y
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X \ Y = X holds
X misses Y
let X, Y be ManySortedSet of I; ::_thesis: ( X \ Y = X implies X misses Y )
assume A1: X \ Y = X ; ::_thesis: X misses Y
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( i in I implies X . i misses Y . i )
assume  i in I ; ::_thesis: X . i misses Y . i
then  (X . i) \ (Y . i) = X . i by A1, Def6;
hence  X . i misses Y . i by XBOOLE_1:83; ::_thesis: verum
end;

theorem :: PBOOLE:118
for I being set
for X, Y being ManySortedSet of I holds X \ Y misses Y \ X
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds X \ Y misses Y \ X
let X, Y be ManySortedSet of I; ::_thesis: X \ Y misses Y \ X
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( i in I implies (X \ Y) . i misses (Y \ X) . i )
assume  i in I ; ::_thesis: (X \ Y) . i misses (Y \ X) . i
then  ( (X \ Y) . i = (X . i) \ (Y . i) & (Y \ X) . i = (Y . i) \ (X . i) ) by Def6;
hence  (X \ Y) . i misses (Y \ X) . i by XBOOLE_1:82; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X c= Y holds
X [= Y
let X, Y be ManySortedSet of I; ::_thesis: ( X c= Y implies X [= Y )
assume A1: X c= Y ; ::_thesis: X [= Y
let x be ManySortedSet of I; :: according to PBOOLE:def_11 ::_thesis: ( x in X implies x in Y )
assume A2: x in X ; ::_thesis: x in Y
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies x . i in Y . i )
assume A3: i in I ; ::_thesis: x . i in Y . i
then A4: X . i c= Y . i by A1, Def2;
 x . i in X . i by A2, A3, Def1;
hence  x . i in Y . i by A4; ::_thesis: verum
end;

theorem :: PBOOLE:120
for I being set
for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z
proof
let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z
let X, Y, Z be ManySortedSet of I; ::_thesis: ( X [= Y & Y [= Z implies X [= Z )
assume that
A1: X [= Y and
A2: Y [= Z ; ::_thesis: X [= Z
let x be ManySortedSet of I; :: according to PBOOLE:def_11 ::_thesis: ( x in X implies x in Z )
assume  x in X ; ::_thesis: x in Z
then  x in Y by A1, Def11;
hence  x in Z by A2, Def11; ::_thesis: verum
end;

begin

theorem :: PBOOLE:121
[[0]] {} in [[0]] {}
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in {} implies ([[0]] {}) . i in ([[0]] {}) . i )
thus  ( i in {} implies ([[0]] {}) . i in ([[0]] {}) . i ) ; ::_thesis: verum
end;

theorem :: PBOOLE:122
for X being ManySortedSet of {} holds X = {}
proof
let X be ManySortedSet of {} ; ::_thesis: X = {}
 dom X = {} by PARTFUN1:def_2;
hence  X = {} by RELAT_1:41; ::_thesis: verum
end;


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
let I be non empty set ; ::_thesis: for X, Y being ManySortedSet of I st X overlaps Y holds
X meets Y
let X, Y be ManySortedSet of I; ::_thesis: ( X overlaps Y implies X meets Y )
set i = the Element of I;
assume  X overlaps Y ; ::_thesis: X meets Y
then  X . the Element of I meets Y . the Element of I by Def7;
hence  X meets Y by Def8; ::_thesis: verum
end;

theorem Th124: :: PBOOLE:124
for I being non empty set
for x being ManySortedSet of I holds not x in [[0]] I
proof
let I be non empty set ; ::_thesis: for x being ManySortedSet of I holds not x in [[0]] I
set i = the Element of I;
given x being ManySortedSet of I such that A1: x in [[0]] I ; ::_thesis: contradiction
 x . the Element of I in ([[0]] I) . the Element of I by A1, Def1;
hence  contradiction by FUNCOP_1:7; ::_thesis: verum
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 <> [[0]] I
proof
let I be non empty set ; ::_thesis: for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X /\ Y <> [[0]] I
let x, X, Y be ManySortedSet of I; ::_thesis: ( x in X & x in Y implies X /\ Y <> [[0]] I )
assume  ( x in X & x in Y ) ; ::_thesis: X /\ Y <> [[0]] I
then  x in X /\ Y by Th8;
hence  X /\ Y <> [[0]] I by Th124; ::_thesis: verum
end;

theorem :: PBOOLE:126
for I being non empty set
for X being ManySortedSet of I holds not X overlaps [[0]] I
proof
let I be non empty set ; ::_thesis: for X being ManySortedSet of I holds not X overlaps [[0]] I
let X be ManySortedSet of I; ::_thesis: not X overlaps [[0]] I
assume  X overlaps [[0]] I ; ::_thesis: contradiction
then  ex x being ManySortedSet of I st
( x in X & x in [[0]] I ) by Th11;
hence  contradiction by Th124; ::_thesis: verum
end;

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
proof
let I be non empty set ; ::_thesis: for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds
not X overlaps Y
let X, Y be ManySortedSet of I; ::_thesis: ( X /\ Y = [[0]] I implies not X overlaps Y )
assume A1: X /\ Y = [[0]] I ; ::_thesis: not X overlaps Y
assume  X overlaps Y ; ::_thesis: contradiction
then consider x being ManySortedSet of I such that
A2: ( x in X & x in Y ) by Th11;
 x in X /\ Y by A2, Th8;
hence  contradiction by A1, Th124; ::_thesis: verum
end;

theorem :: PBOOLE:128
for I being non empty set
for X being ManySortedSet of I st X overlaps X holds
X <> [[0]] I
proof
let I be non empty set ; ::_thesis: for X being ManySortedSet of I st X overlaps X holds
X <> [[0]] I
let X be ManySortedSet of I; ::_thesis: ( X overlaps X implies X <> [[0]] I )
 X = X /\ X ;
hence  ( X overlaps X implies X <> [[0]] I ) by Th127; ::_thesis: verum
end;

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 )
proof
 dom X = I by PARTFUN1:def_2;
hence  ( X is empty-yielding iff for i being set st i in I holds
X . i is empty ) by FUNCT_1:def_8; ::_thesis: verum
end;
:: 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 )
proof
 dom X = I by PARTFUN1:def_2;
hence  ( X is non-empty iff for i being set st i in I holds
not X . i is empty ) by FUNCT_1:def_9; ::_thesis: verum
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 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()
proof
take  [[0]] I ; ::_thesis: [[0]] I is V9()
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( i in I implies ([[0]] I) . i is empty )
assume  i in I ; ::_thesis: ([[0]] I) . i is empty
thus  ([[0]] I) . i is empty by Th5; ::_thesis: verum
end;
cluster Relation-like V8() I -defined Function-like total for set ;
existence
 not for b1 being ManySortedSet of I holds b1 is V8()
proof
set e = the set ;
reconsider M = I --> { the set } as ManySortedSet of I ;
take  M ; ::_thesis: M is V8()
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( i in I implies not M . i is empty )
assume  i in I ; ::_thesis: not M . i is empty
hence  not M . i is empty by FUNCOP_1:7; ::_thesis: verum
end;
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()
proof
set i = the Element of I;
let M be ManySortedSet of I; ::_thesis: ( M is V8() implies not M is V9() )
assume A1: M is V8() ; ::_thesis: M is V9()
take  the Element of I ; :: according to PBOOLE:def_12 ::_thesis: ( the Element of I in I & not M . the Element of I is empty )
thus  the Element of I in I ; ::_thesis: not M . the Element of I is empty
thus  not M . the Element of I is empty by A1, Def13; ::_thesis: verum
end;
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 )
proof
let I be set ; ::_thesis: for X being ManySortedSet of I holds
( X is V9() iff X = [[0]] I )
let X be ManySortedSet of I; ::_thesis: ( X is V9() iff X = [[0]] I )
hereby  ::_thesis: ( X = [[0]] I implies X is V9() )
assume  X is V9() ; ::_thesis: X = [[0]] I
then  for i being set st i in I holds
X . i = {} ;
hence  X = [[0]] I by Th6; ::_thesis: verum
end;
assume A1: X = [[0]] I ; ::_thesis: X is V9()
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( i in I implies X . i is empty )
assume  i in I ; ::_thesis: X . i is empty
thus  X . i is empty by A1, Th5; ::_thesis: verum
end;

theorem :: PBOOLE:130
for I being set
for Y, X being ManySortedSet of I st Y is V9() & X c= Y holds
X is V9()
proof
let I be set ; ::_thesis: for Y, X being ManySortedSet of I st Y is V9() & X c= Y holds
X is V9()
let Y, X be ManySortedSet of I; ::_thesis: ( Y is V9() & X c= Y implies X is V9() )
assume A1: ( Y is V9() & X c= Y ) ; ::_thesis: X is V9()
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( i in I implies X . i is empty )
assume  i in I ; ::_thesis: X . i is empty
then  ( X . i c= Y . i & Y . i is empty ) by A1, Def2;
hence  X . i is empty by XBOOLE_1:3; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X is V8() & X c= Y holds
Y is V8()
let X, Y be ManySortedSet of I; ::_thesis: ( X is V8() & X c= Y implies Y is V8() )
assume A1: ( X is V8() & X c= Y ) ; ::_thesis: Y is V8()
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( i in I implies not Y . i is empty )
assume  i in I ; ::_thesis: not Y . i is empty
then  ( X . i c= Y . i & not X . i is empty ) by A1, Def2, Def13;
hence  not Y . i is empty by XBOOLE_1:3; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X is V8() & X [= Y holds
X c= Y
let X, Y be ManySortedSet of I; ::_thesis: ( X is V8() & X [= Y implies X c= Y )
assume that
A1: X is V8() and
A2: X [= Y ; ::_thesis: X c= Y
deffunc H1( set ) ->  set = X . $1;
A3: for i being set st i in I holds
H1(i) <> {} by A1, Def13;
consider f being ManySortedSet of I such that
A4: for i being set st i in I holds
f . i in H1(i) from PBOOLE:sch_1(A3);
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( i in I implies X . i c= Y . i )
assume A5: i in I ; ::_thesis: X . i c= Y . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X . i or e in Y . i )
deffunc H2( set ) ->  set = IFEQ (i,$1,e,(f . $1));
consider g being Function such that
A6: dom g = I and
A7: for u being set st u in I holds
g . u = H2(u) from FUNCT_1:sch_3();
reconsider g = g as ManySortedSet of I by A6, PARTFUN1:def_2, RELAT_1:def_18;
A8: g . i = IFEQ (i,i,e,(f . i)) by A5, A7
.= e by FUNCOP_1:def_8 ;
assume A9: e in X . i ; ::_thesis: e in Y . i
 g in X
proof
let u be set ; :: according to PBOOLE:def_1 ::_thesis: ( u in I implies g . u in X . u )
assume A10: u in I ; ::_thesis: g . u in X . u
percases ( u = i or u <> i ) ;
suppose u = i ; ::_thesis: g . u in X . u
hence  g . u in X . u by A8, A9; ::_thesis: verum
end;
supposeA11: u <> i ; ::_thesis: g . u in X . u
g . u = IFEQ (i,u,e,(f . u)) by A7, A10
.= f . u by A11, FUNCOP_1:def_8 ;
hence  g . u in X . u by A4, A10; ::_thesis: verum
end;
end;
end;
then  g in Y by A2, Def11;
hence  e in Y . i by A5, A8, Def1; ::_thesis: verum
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
let I be set ; ::_thesis: for X, Y being ManySortedSet of I st X is V8() & X [= Y holds
Y is V8()
let X, Y be ManySortedSet of I; ::_thesis: ( X is V8() & X [= Y implies Y is V8() )
assume A1: X is V8() ; ::_thesis: ( not X [= Y or not Y is V8() )
assume  X [= Y ; ::_thesis: Y is V8()
then  X c= Y by A1, Th132;
hence  Y is V8() by A1, Th131; ::_thesis: verum
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
let I be set ; ::_thesis: for X being V8() ManySortedSet of I ex x being ManySortedSet of I st x in X
let X be V8() ManySortedSet of I; ::_thesis: ex x being ManySortedSet of I st x in X
deffunc H1( set ) ->  set = X . $1;
A1: for i being set st i in I holds
H1(i) <> {} by Def13;
consider f being ManySortedSet of I such that
A2: for i being set st i in I holds
f . i in H1(i) from PBOOLE:sch_1(A1);
take  f ; ::_thesis: f in X
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( i in I implies f . i in X . i )
thus  ( i in I implies f . i in X . i ) by A2; ::_thesis: verum
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
let I be set ; ::_thesis: 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
let Y be ManySortedSet of I; ::_thesis: 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
let X be V8() ManySortedSet of I; ::_thesis: ( ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) implies X = Y )
deffunc H1( set ) ->  set = X . $1;
A1: for i being set st i in I holds
H1(i) <> {} by Def13;
consider f being ManySortedSet of I such that
A2: for i being set st i in I holds
f . i in H1(i) from PBOOLE:sch_1(A1);
assume A3: for x being ManySortedSet of I holds
( x in X iff x in Y ) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A4: i in I ; ::_thesis: X . i = Y . i
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_X_._i_implies_e_in_Y_._i_)_&_(_e_in_Y_._i_implies_e_in_X_._i_)_)
let e be set ; ::_thesis: ( ( e in X . i implies e in Y . i ) & ( e in Y . i implies e in X . i ) )
deffunc H2( set ) ->  set = IFEQ (i,$1,e,(f . $1));
consider g being Function such that
A5: dom g = I and
A6: for u being set st u in I holds
g . u = H2(u) from FUNCT_1:sch_3();
reconsider g = g as ManySortedSet of I by A5, PARTFUN1:def_2, RELAT_1:def_18;
A7: g . i = IFEQ (i,i,e,(f . i)) by A4, A6
.= e by FUNCOP_1:def_8 ;
hereby  ::_thesis: ( e in Y . i implies e in X . i )
assume A8: e in X . i ; ::_thesis: e in Y . i
 g in X
proof
let u be set ; :: according to PBOOLE:def_1 ::_thesis: ( u in I implies g . u in X . u )
assume A9: u in I ; ::_thesis: g . u in X . u
percases ( u = i or u <> i ) ;
suppose u = i ; ::_thesis: g . u in X . u
hence  g . u in X . u by A7, A8; ::_thesis: verum
end;
supposeA10: u <> i ; ::_thesis: g . u in X . u
g . u = IFEQ (i,u,e,(f . u)) by A6, A9
.= f . u by A10, FUNCOP_1:def_8 ;
hence  g . u in X . u by A2, A9; ::_thesis: verum
end;
end;
end;
then  g in Y by A3;
hence  e in Y . i by A4, A7, Def1; ::_thesis: verum
end;
assume A11: e in Y . i ; ::_thesis: e in X . i
 g in Y
proof
let u be set ; :: according to PBOOLE:def_1 ::_thesis: ( u in I implies g . u in Y . u )
assume A12: u in I ; ::_thesis: g . u in Y . u
percases ( u = i or u <> i ) ;
suppose u = i ; ::_thesis: g . u in Y . u
hence  g . u in Y . u by A7, A11; ::_thesis: verum
end;
supposeA13: u <> i ; ::_thesis: g . u in Y . u
 f in X by A2, Def1;
then A14: f in Y by A3;
g . u = IFEQ (i,u,e,(f . u)) by A6, A12
.= f . u by A13, FUNCOP_1:def_8 ;
hence  g . u in Y . u by A12, A14, Def1; ::_thesis: verum
end;
end;
end;
then  g in X by A3;
hence  e in X . i by A4, A7, Def1; ::_thesis: verum
end;
hence  X . i = Y . i by TARSKI:1; ::_thesis: verum
end;
hence  X = Y by Th3; ::_thesis: verum
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
let I be set ; ::_thesis: 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
let Y, Z be ManySortedSet of I; ::_thesis: 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
let X be V8() ManySortedSet of I; ::_thesis: ( ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) implies X = Y /\ Z )
assume A1: for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ; ::_thesis: X = Y /\ Z
now__::_thesis:_for_x_being_ManySortedSet_of_I_holds_
(_(_x_in_X_implies_x_in_Y_/\_Z_)_&_(_x_in_Y_/\_Z_implies_x_in_X_)_)
let x be ManySortedSet of I; ::_thesis: ( ( x in X implies x in Y /\ Z ) & ( x in Y /\ Z implies x in X ) )
hereby  ::_thesis: ( x in Y /\ Z implies x in X )
assume  x in X ; ::_thesis: x in Y /\ Z
then  ( x in Y & x in Z ) by A1;
hence  x in Y /\ Z by Th8; ::_thesis: verum
end;
assume  x in Y /\ Z ; ::_thesis: x in X
then  ( x in Y & x in Z ) by Th8;
hence  x in X by A1; ::_thesis: verum
end;
hence  X = Y /\ Z by Th135; ::_thesis: verum
end;

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]
proof
A2: for i being set st i in F1() holds
ex j being set st P1[i,j] by A1;
consider f being Function such that
A3: dom f = F1() and
A4: for i being set st i in F1() holds
P1[i,f . i] from CLASSES1:sch_1(A2);
reconsider f = f as ManySortedSet of F1() by A3, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for i being set st i in F1() holds
P1[i,f . i]
thus  for i being set st i in F1() holds
P1[i,f . i] by A4; ::_thesis: verum
end;

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)
proof
consider f being Function such that
A1: dom f = F1() and
A2: for i being set st i in F1() holds
f . i = F2(i) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of F1() by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for i being set st i in F1() holds
f . i = F2(i)
thus  for i being set st i in F1() holds
f . i = F2(i) by A2; ::_thesis: verum
end;

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
proof
set f = the Function;
reconsider F = I --> the Function as ManySortedSet of I ;
take  F ; ::_thesis: F is Function-yielding
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom F or F . x is set )
assume  x in dom F ; ::_thesis: F . x is set
thus  F . x is set ; ::_thesis: verum
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
let I be set ; ::_thesis: for M being V8() ManySortedSet of I holds not {} in rng M
let M be V8() ManySortedSet of I; ::_thesis: not {} in rng M
A1: dom M = I by PARTFUN1:def_2;
assume  {} in rng M ; ::_thesis: contradiction
then  ex i being set st
( i in I & M . i = {} ) by A1, FUNCT_1:def_3;
hence  contradiction by Def13; ::_thesis: verum
end;

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 & A = M . i )
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for A being Component of M ex i being set st
( i in I & A = M . i )
let M be ManySortedSet of I; ::_thesis: for A being Component of M ex i being set st
( i in I & A = M . i )
let A be Component of M; ::_thesis: ex i being set st
( i in I & A = M . i )
A1: dom M = I by PARTFUN1:def_2;
then  rng M <> {} by RELAT_1:42;
hence  ex i being set st
( i in I & A = M . i ) by A1, FUNCT_1:def_3; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for i being set st i in I holds
M . i is Component of M
let M be ManySortedSet of I; ::_thesis: for i being set st i in I holds
M . i is Component of M
let i be set ; ::_thesis: ( i in I implies M . i is Component of M )
assume A1: i in I ; ::_thesis: M . i is Component of M
 dom M = I by PARTFUN1:def_2;
hence  M . i is Component of M by A1, FUNCT_1:def_3; ::_thesis: verum
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 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
proof
defpred S1[ set , set ] means $2 is Element of B . $1;
A1: for i being set st i in I holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume  i in I ; ::_thesis: ex j being set st S1[i,j]
set j = the Element of B . i;
reconsider j = the Element of B . i as set ;
take  j ; ::_thesis: S1[i,j]
thus  S1[i,j] ; ::_thesis: verum
end;
thus  ex f being ManySortedSet of I st
for i being set st i in I holds
S1[i,f . i] from PBOOLE:sch_3(A1); ::_thesis: verum
end;
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);
proof
defpred S1[ set , set ] means $2 is Function of (A . $1),(B . $1);
A1: for i being set st i in I holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume  i in I ; ::_thesis: ex j being set st S1[i,j]
set j = the Function of (A . i),(B . i);
reconsider j = the Function of (A . i),(B . i) as set ;
take  j ; ::_thesis: S1[i,j]
thus  S1[i,j] ; ::_thesis: verum
end;
consider f being ManySortedSet of I such that
A2: for i being set st i in I holds
S1[i,f . i] from PBOOLE:sch_3(A1);
 f is Function-yielding
proof
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom f or f . i is set )
assume  i in dom f ; ::_thesis: f . i is set
then  i in I by PARTFUN1:def_2;
hence  f . i is set by A2; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of I ;
take  f ; ::_thesis: for i being set st i in I holds
f . i is Function of (A . i),(B . i)
let i be set ; ::_thesis: ( i in I implies f . i is Function of (A . i),(B . i) )
assume  i in I ; ::_thesis: f . i is Function of (A . i),(B . i)
hence  f . i is Function of (A . i),(B . i) by A2; ::_thesis: verum
end;
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
proof
let f be ManySortedFunction of A,B; ::_thesis: f is Function-yielding
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom f or f . i is set )
assume  i in dom f ; ::_thesis: f . i is set
then  i in I by PARTFUN1:def_2;
hence  f . i is set by Def15; ::_thesis: verum
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;
clusterO * F -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = F * O holds
b1 is total
proof
A1: dom F = J by PARTFUN1:def_2;
 ( rng O c= J & dom O = I ) by FUNCT_2:def_1, RELAT_1:def_19;
then  dom (F * O) = I by A1, RELAT_1:27;
hence  for b1 being I -defined Function st b1 = F * O holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
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)
proof
consider f being Function such that
A1: dom f = F1() and
A2: for d being Element of F1() holds f . d = F2(d) from FUNCT_1:sch_4();
 f is ManySortedSet of F1() by A1, PARTFUN1:def_2, RELAT_1:def_18;
hence  ex X being ManySortedSet of F1() st
for d being Element of F1() holds X . d = F2(d) by A2; ::_thesis: verum
end;

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):]
proof
deffunc H1( set ) ->  set = [:(X . $1),(Y . $1):];
consider f being Function such that
A1: ( dom f = I & ( for i being set st i in I holds
f . i = H1(i) ) ) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for i being set st i in I holds
f . i = [:(X . i),(Y . i):]
thus  for i being set st i in I holds
f . i = [:(X . i),(Y . i):] by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = [:(X . i),(Y . i):] ) & ( for i being set st i in I holds
b2 . i = [:(X . i),(Y . i):] ) holds
b1 = b2
proof
let f, g be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
f . i = [:(X . i),(Y . i):] ) & ( for i being set st i in I holds
g . i = [:(X . i),(Y . i):] ) implies f = g )
assume that
A2: for i being set st i in I holds
f . i = [:(X . i),(Y . i):] and
A3: for i being set st i in I holds
g . i = [:(X . i),(Y . i):] ; ::_thesis: f = g
 for x being set st x in I holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in I implies f . x = g . x )
assume A4: x in I ; ::_thesis: f . x = g . x
then  f . x = [:(X . x),(Y . x):] by A2;
hence  f . x = g . x by A3, A4; ::_thesis: verum
end;
hence  f = g by Th3; ::_thesis: verum
end;
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))
proof
thus  ex M being ManySortedSet of I st
for i being set st i in I holds
M . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum
end;
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)) ) & ( for i being set st i in I holds
b2 . i = Funcs ((X . i),(Y . i)) ) holds
b1 = b2
proof
let F1, F2 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
F1 . i = Funcs ((X . i),(Y . i)) ) & ( for i being set st i in I holds
F2 . i = Funcs ((X . i),(Y . i)) ) implies F1 = F2 )
assume that
A1: for i being set st i in I holds
F1 . i = Funcs ((X . i),(Y . i)) and
A2: for i being set st i in I holds
F2 . i = Funcs ((X . i),(Y . i)) ; ::_thesis: F1 = F2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F1_._i_=_F2_._i
let i be set ; ::_thesis: ( i in I implies F1 . i = F2 . i )
assume A3: i in I ; ::_thesis: F1 . i = F2 . i
hence F1 . i = Funcs ((X . i),(Y . i)) by A1
.= F2 . i by A2, A3 ;
::_thesis: verum
end;
hence  F1 = F2 by Th3; ::_thesis: verum
end;
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()
proof
reconsider N = M as ManySortedSubset of M by Def18;
take  N ; ::_thesis: N is V8()
thus  N is V8() ; ::_thesis: verum
end;
end;

definition
let F, G be Function-yielding Function;
funcG ** F ->  Function means :Def19: :: PBOOLE:def 19
( dom it = (dom F) /\ (dom G) & ( 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) & ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) )
proof
defpred S1[ set , set ] means $2 = (G . $1) * (F . $1);
A1: for i being set st i in (dom F) /\ (dom G) holds
ex u being set st S1[i,u] ;
 ex H being Function st
( dom H = (dom F) /\ (dom G) & ( for i being set st i in (dom F) /\ (dom G) holds
S1[i,H . i] ) ) from CLASSES1:sch_1(A1);
hence  ex b1 being Function st
( dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
b1 . i = (G . i) * (F . i) ) & dom b2 = (dom F) /\ (dom G) & ( for i being set st i in dom b2 holds
b2 . i = (G . i) * (F . i) ) holds
b1 = b2
proof
let H1, H2 be Function; ::_thesis: ( dom H1 = (dom F) /\ (dom G) & ( for i being set st i in dom H1 holds
H1 . i = (G . i) * (F . i) ) & dom H2 = (dom F) /\ (dom G) & ( for i being set st i in dom H2 holds
H2 . i = (G . i) * (F . i) ) implies H1 = H2 )
assume that
A2: dom H1 = (dom F) /\ (dom G) and
A3: for i being set st i in dom H1 holds
H1 . i = (G . i) * (F . i) and
A4: dom H2 = (dom F) /\ (dom G) and
A5: for i being set st i in dom H2 holds
H2 . i = (G . i) * (F . i) ; ::_thesis: H1 = H2
now__::_thesis:_for_i_being_set_st_i_in_(dom_F)_/\_(dom_G)_holds_
H1_._i_=_H2_._i
let i be set ; ::_thesis: ( i in (dom F) /\ (dom G) implies H1 . i = H2 . i )
reconsider f = F . i as Function ;
reconsider g = G . i as Function ;
assume A6: i in (dom F) /\ (dom G) ; ::_thesis: H1 . i = H2 . i
then  H1 . i = g * f by A2, A3;
hence  H1 . i = H2 . i by A4, A5, A6; ::_thesis: verum
end;
hence  H1 = H2 by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
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) & ( 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
proof
set H = G ** F;
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (G ** F) or (G ** F) . x is set )
reconsider f = F . x as Function ;
reconsider g = G . x as Function ;
assume  x in dom (G ** F) ; ::_thesis: (G ** F) . x is set
then  (G ** F) . x = g * f by Def19;
hence  (G ** F) . x is set ; ::_thesis: verum
end;
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)
proof
defpred S1[ set , set ] means $2 = (F . $1) .: (A . $1);
A1: for i being set st i in I holds
ex u being set st S1[i,u] ;
consider g being Function such that
A2: ( dom g = I & ( for i being set st i in I holds
S1[i,g . i] ) ) from CLASSES1:sch_1(A1);
reconsider g = g as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
take  g ; ::_thesis: for i being set st i in I holds
g . i = (F . i) .: (A . i)
thus  for i being set st i in I holds
g . i = (F . i) .: (A . i) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds
b2 . i = (F . i) .: (A . i) ) holds
b1 = b2
proof
let B, B1 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
B . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds
B1 . i = (F . i) .: (A . i) ) implies B = B1 )
assume that
A3: for i being set st i in I holds
B . i = (F . i) .: (A . i) and
A4: for i being set st i in I holds
B1 . i = (F . i) .: (A . i) ; ::_thesis: B = B1
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
B_._i_=_B1_._i
let i be set ; ::_thesis: ( i in I implies B . i = B1 . i )
reconsider f = F . i as Function ;
assume A5: i in I ; ::_thesis: B . i = B1 . i
then  B . i = f .: (A . i) by A3;
hence  B . i = B1 . i by A4, A5; ::_thesis: verum
end;
hence  B = B1 by Th3; ::_thesis: verum
end;
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
proof
 rng ([[0]] I) c= {{}} by FUNCOP_1:13;
hence  [[0]] I is empty-yielding by RELAT_1:def_15; ::_thesis: verum
end;
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]
proof
defpred S1[ set , set ] means P1[$1,$2];
A2: for i being set st i in F1() holds
ex j being set st S1[i,j] by A1;
consider f being ManySortedSet of F1() such that
A3: for i being set st i in F1() holds
S1[i,f . i] from PBOOLE:sch_3(A2);
take  f ; ::_thesis: for i being Element of F1() holds P1[i,f . i]
let i be Element of F1(); ::_thesis: P1[i,f . i]
thus  P1[i,f . i] by A3; ::_thesis: verum
end;

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
proof
set x = the Element of X;
let f be ManySortedSet of X; ::_thesis: not f is empty
 dom f = X by PARTFUN1:def_2;
then  [ the Element of X,(f . the Element of X)] in f by FUNCT_1:def_2;
hence  not f is empty ; ::_thesis: verum
end;
end;

theorem :: PBOOLE:140
for F, G, H being Function-yielding Function holds (H ** G) ** F = H ** (G ** F)
proof
let F, G, H be Function-yielding Function; ::_thesis: (H ** G) ** F = H ** (G ** F)
set f = (H ** G) ** F;
set g = H ** (G ** F);
now__::_thesis:_(_dom_((H_**_G)_**_F)_=_dom_(H_**_(G_**_F))_&_(_for_x_being_set_st_x_in_dom_((H_**_G)_**_F)_holds_
((H_**_G)_**_F)_._x_=_(H_**_(G_**_F))_._x_)_)
A1: dom ((H ** G) ** F) = (dom (H ** G)) /\ (dom F) by Def19
.= ((dom H) /\ (dom G)) /\ (dom F) by Def19 ;
then A2: dom ((H ** G) ** F) = (dom H) /\ ((dom G) /\ (dom F)) by XBOOLE_1:16;
hence A3: dom ((H ** G) ** F) = (dom H) /\ (dom (G ** F)) by Def19
.= dom (H ** (G ** F)) by Def19 ;
::_thesis: for x being set st x in dom ((H ** G) ** F) holds
((H ** G) ** F) . x = (H ** (G ** F)) . x
let x be set ; ::_thesis: ( x in dom ((H ** G) ** F) implies ((H ** G) ** F) . x = (H ** (G ** F)) . x )
assume A4: x in dom ((H ** G) ** F) ; ::_thesis: ((H ** G) ** F) . x = (H ** (G ** F)) . x
then  x in (dom H) /\ (dom G) by A1, XBOOLE_0:def_4;
then A5: x in dom (H ** G) by Def19;
 x in (dom G) /\ (dom F) by A2, A4, XBOOLE_0:def_4;
then A6: x in dom (G ** F) by Def19;
thus ((H ** G) ** F) . x = ((H ** G) . x) * (F . x) by A4, Def19
.= ((H . x) * (G . x)) * (F . x) by A5, Def19
.= (H . x) * ((G . x) * (F . x)) by RELAT_1:36
.= (H . x) * ((G ** F) . x) by A6, Def19
.= (H ** (G ** F)) . x by A3, A4, Def19 ; ::_thesis: verum
end;
hence  (H ** G) ** F = H ** (G ** F) by FUNCT_1:2; ::_thesis: verum
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 b1 being I -defined f -compatible Function st b1 is total
proof
deffunc H1( set ) ->  set = f . I;
A1: for e being set st e in I holds
H1(e) <> {} ;
consider g being ManySortedSet of I such that
A2: for e being set st e in I holds
g . e in H1(e) from PBOOLE:sch_1(A1);
 g is f -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom g or g . x in f . x )
assume  x in dom g ; ::_thesis: g . x in f . x
then  x in I by PARTFUN1:def_2;
hence  g . x in f . x by A2; ::_thesis: verum
end;
then reconsider g = g as I -defined f -compatible Function ;
take  g ; ::_thesis: g is total
thus  g is total ; ::_thesis: verum
end;
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
proof
let I be set ; ::_thesis: for f being V8() ManySortedSet of I
for p being I -defined b1 -compatible Function ex s being b1 -compatible ManySortedSet of I st p c= s
let f be V8() ManySortedSet of I; ::_thesis: for p being I -defined f -compatible Function ex s being f -compatible ManySortedSet of I st p c= s
let p be I -defined f -compatible Function; ::_thesis: ex s being f -compatible ManySortedSet of I st p c= s
set h = the f -compatible ManySortedSet of I;
take  the f -compatible ManySortedSet of I +* p ; ::_thesis: p c= the f -compatible ManySortedSet of I +* p
thus  p c= the f -compatible ManySortedSet of I +* p by FUNCT_4:25; ::_thesis: verum
end;

theorem :: PBOOLE:142
for I, A being set
for s, ss being ManySortedSet of I holds (ss +* (s | A)) | A = s | A
proof
let I, A be set ; ::_thesis: for s, ss being ManySortedSet of I holds (ss +* (s | A)) | A = s | A
let s, ss be ManySortedSet of I; ::_thesis: (ss +* (s | A)) | A = s | A
dom s = I by PARTFUN1:def_2
.= dom ss by PARTFUN1:def_2 ;
then  A /\ (dom ss) c= A /\ (dom s) ;
hence  (ss +* (s | A)) | A = s | A by FUNCT_4:88; ::_thesis: verum
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 b1 being ManySortedSet of Y st b1 is X -valued
proof
take M = Y --> the Element of X; ::_thesis: M is X -valued
A1: { the Element of X} c= X by ZFMISC_1:31;
 rng M c= { the Element of X} by FUNCOP_1:13;
hence  rng M c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
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
proof
let I, Y be non empty set ; ::_thesis: for M being Y -valued ManySortedSet of I
for x being Element of I holds M . x = M /. x
let M be Y -valued ManySortedSet of I; ::_thesis: for x being Element of I holds M . x = M /. x
let x be Element of I; ::_thesis: M . x = M /. x
 dom M = I by PARTFUN1:def_2;
hence  M . x = M /. x by PARTFUN1:def_6; ::_thesis: verum
end;

theorem :: PBOOLE:144
for I being set
for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M
proof
let I be set ; ::_thesis: for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M
let f be Function; ::_thesis: for M being ManySortedSet of I holds (f +* M) | I = M
let M be ManySortedSet of I; ::_thesis: (f +* M) | I = M
A1: dom (f | I) c= I by RELAT_1:58;
A2: dom M = I by PARTFUN1:def_2;
thus (f +* M) | I = (f | I) +* (M | I) by FUNCT_4:71
.= (f | I) +* M by A2, RELAT_1:69
.= M by A1, A2, FUNCT_4:19 ; ::_thesis: verum
end;

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
proof
let I be set ; ::_thesis: for Y being non empty set
for p being I -defined b1 -valued Function ex s being b1 -valued ManySortedSet of I st p c= s
let Y be non empty set ; ::_thesis: for p being I -defined Y -valued Function ex s being Y -valued ManySortedSet of I st p c= s
let p be I -defined Y -valued Function; ::_thesis: ex s being Y -valued ManySortedSet of I st p c= s
set h = the Y -valued ManySortedSet of I;
take  the Y -valued ManySortedSet of I +* p ; ::_thesis: p c= the Y -valued ManySortedSet of I +* p
thus  p c= the Y -valued ManySortedSet of I +* p by FUNCT_4:25; ::_thesis: verum
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 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 )
proof
thus  ( A = B implies for i being Element of I holds A . i = B . i ) ; ::_thesis: ( ( for i being Element of I holds A . i = B . i ) implies A = B )
assume  for i being Element of I holds A . i = B . i ; ::_thesis: A = B
then  for i being set st i in I holds
A . i = B . i ;
hence  A = B by Th3; ::_thesis: verum
end;
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 );