:: by Andrzej Trybulec

::

:: Received July 7, 1993

:: Copyright (c) 1993-2018 Association of Mizar Users

registration
end;

definition

let I be set ;

let X, Y be ManySortedSet of I;

reflexivity

for X being ManySortedSet of I

for i being object st i in I holds

X . i c= X . i ;

end;
let X, Y be ManySortedSet of I;

reflexivity

for X being ManySortedSet of I

for i being object st i in I holds

X . i c= X . i ;

:: deftheorem defines in PBOOLE:def 1 :

for I being set

for X, Y being ManySortedSet of I holds

( X in Y iff for i being object st i in I holds

X . i in Y . i );

for I being set

for X, Y being ManySortedSet of I holds

( X in Y iff for i being object st i in I holds

X . i in Y . i );

:: deftheorem defines c= PBOOLE:def 2 :

for I being set

for X, Y being ManySortedSet of I holds

( X c= Y iff for i being object st i in I holds

X . i c= Y . i );

for I being set

for X, Y being ManySortedSet of I holds

( X c= Y iff for i being object st i in I holds

X . i c= Y . i );

definition

let I be non empty set ;

let X, Y be ManySortedSet of I;

:: original: in

redefine pred X in Y;

asymmetry

for X, Y being ManySortedSet of I st (I,b_{1},b_{2}) holds

not (I,b_{2},b_{1})

end;
let X, Y be ManySortedSet of I;

:: original: in

redefine pred X in Y;

asymmetry

for X, Y being ManySortedSet of I st (I,b

not (I,b

proof end;

scheme :: PBOOLE:sch 2

PSeparation{ F_{1}() -> set , F_{2}() -> ManySortedSet of F_{1}(), P_{1}[ object , object ] } :

PSeparation{ F

ex X being ManySortedSet of F_{1}() st

for i being object st i in F_{1}() holds

for e being object holds

( e in X . i iff ( e in F_{2}() . i & P_{1}[i,e] ) )

for i being object st i in F

for e being object holds

( e in X . i iff ( e in F

proof end;

theorem Th3: :: PBOOLE:3

for I being set

for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i = Y . i ) holds

X = Y

for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i = Y . i ) holds

X = Y

proof end;

definition

let I be set ;

coherence

I --> {} is ManySortedSet of I ;

correctness

;

let X, Y be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = (X . i) \/ (Y . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = (X . i) \/ (Y . i) ) & ( for i being object st i in I holds

b_{2} . i = (X . i) \/ (Y . i) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = (X . i) \/ (Y . i) ) holds

for i being object st i in I holds

b_{1} . i = (Y . i) \/ (X . i)
;

idempotence

for X being ManySortedSet of I

for i being object st i in I holds

X . i = (X . i) \/ (X . i) ;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = (X . i) /\ (Y . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = (X . i) /\ (Y . i) ) & ( for i being object st i in I holds

b_{2} . i = (X . i) /\ (Y . i) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = (X . i) /\ (Y . i) ) holds

for i being object st i in I holds

b_{1} . i = (Y . i) /\ (X . i)
;

idempotence

for X being ManySortedSet of I

for i being object st i in I holds

X . i = (X . i) /\ (X . i) ;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = (X . i) \ (Y . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = (X . i) \ (Y . i) ) & ( for i being object st i in I holds

b_{2} . i = (X . i) \ (Y . i) ) holds

b_{1} = b_{2}

for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i meets Y . i ) holds

for i being object st i in I holds

Y . i meets X . i ;

symmetry

for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i misses Y . i ) holds

for i being object st i in I holds

Y . i misses X . i ;

end;
coherence

I --> {} is ManySortedSet of I ;

correctness

;

let X, Y be ManySortedSet of I;

func X (\/) Y -> ManySortedSet of I means :Def4: :: PBOOLE:def 4

for i being object st i in I holds

it . i = (X . i) \/ (Y . i);

existence for i being object st i in I holds

it . i = (X . i) \/ (Y . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

for i being object st i in I holds

b

idempotence

for X being ManySortedSet of I

for i being object st i in I holds

X . i = (X . i) \/ (X . i) ;

func X (/\) Y -> ManySortedSet of I means :Def5: :: PBOOLE:def 5

for i being object st i in I holds

it . i = (X . i) /\ (Y . i);

existence for i being object st i in I holds

it . i = (X . i) /\ (Y . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

for i being object st i in I holds

b

idempotence

for X being ManySortedSet of I

for i being object st i in I holds

X . i = (X . i) /\ (X . i) ;

func X (\) Y -> ManySortedSet of I means :Def6: :: PBOOLE:def 6

for i being object st i in I holds

it . i = (X . i) \ (Y . i);

existence for i being object st i in I holds

it . i = (X . i) \ (Y . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

symmetry for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i meets Y . i ) holds

for i being object st i in I holds

Y . i meets X . i ;

symmetry

for X, Y being ManySortedSet of I st ( for i being object st i in I holds

X . i misses Y . i ) holds

for i being object st i in I holds

Y . i misses X . i ;

:: deftheorem Def4 defines (\/) PBOOLE:def 4 :

for I being set

for X, Y, b_{4} being ManySortedSet of I holds

( b_{4} = X (\/) Y iff for i being object st i in I holds

b_{4} . i = (X . i) \/ (Y . i) );

for I being set

for X, Y, b

( b

b

:: deftheorem Def5 defines (/\) PBOOLE:def 5 :

for I being set

for X, Y, b_{4} being ManySortedSet of I holds

( b_{4} = X (/\) Y iff for i being object st i in I holds

b_{4} . i = (X . i) /\ (Y . i) );

for I being set

for X, Y, b

( b

b

:: deftheorem Def6 defines (\) PBOOLE:def 6 :

for I being set

for X, Y, b_{4} being ManySortedSet of I holds

( b_{4} = X (\) Y iff for i being object st i in I holds

b_{4} . i = (X . i) \ (Y . i) );

for I being set

for X, Y, b

( b

b

:: deftheorem defines overlaps PBOOLE:def 7 :

for I being set

for X, Y being ManySortedSet of I holds

( X overlaps Y iff for i being object st i in I holds

X . i meets Y . i );

for I being set

for X, Y being ManySortedSet of I holds

( X overlaps Y iff for i being object st i in I holds

X . i meets Y . i );

:: deftheorem defines misses PBOOLE:def 8 :

for I being set

for X, Y being ManySortedSet of I holds

( X misses Y iff for i being object st i in I holds

X . i misses Y . i );

for I being set

for X, Y being ManySortedSet of I holds

( X misses Y iff for i being object st i in I holds

X . i misses Y . i );

definition

let I be set ;

let X, Y be ManySortedSet of I;

correctness

coherence

(X (\) Y) (\/) (Y (\) X) is ManySortedSet of I;

;

commutativity

for b_{1}, X, Y being ManySortedSet of I st b_{1} = (X (\) Y) (\/) (Y (\) X) holds

b_{1} = (Y (\) X) (\/) (X (\) Y)
;

end;
let X, Y be ManySortedSet of I;

correctness

coherence

(X (\) Y) (\/) (Y (\) X) is ManySortedSet of I;

;

commutativity

for b

b

:: deftheorem defines (\+\) PBOOLE:def 9 :

for I being set

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

for I being set

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

theorem Th4: :: PBOOLE:4

for I being set

for X, Y being ManySortedSet of I

for i being object st i in I holds

(X (\+\) Y) . i = (X . i) \+\ (Y . i)

for X, Y being ManySortedSet of I

for i being object st i in I holds

(X (\+\) Y) . i = (X . i) \+\ (Y . i)

proof end;

theorem Th6: :: PBOOLE:6

for I being set

for X being ManySortedSet of I st ( for i being object st i in I holds

X . i = {} ) holds

X = EmptyMS I

for X being ManySortedSet of I st ( for i being object st i in I holds

X . i = {} ) holds

X = EmptyMS I

proof end;

theorem 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 ) )

for x, X, Y being ManySortedSet of I holds

( x in X (/\) Y iff ( x in X & x in Y ) )

proof end;

theorem Th11: :: PBOOLE:11

for I being set

for X, Y being ManySortedSet of I st X overlaps Y holds

ex x being ManySortedSet of I st

( x in X & x in Y )

for X, Y being ManySortedSet of I st X overlaps Y holds

ex x being ManySortedSet of I st

( x in X & x in Y )

proof end;

Lm1: for I being set

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

X = Y

proof end;

definition

let I be set ;

let X, Y be ManySortedSet of I;

( X = Y iff for i being object st i in I holds

X . i = Y . i ) by Th3;

end;
let X, Y be ManySortedSet of I;

:: original: =

redefine pred X = Y means :: PBOOLE:def 10

for i being object st i in I holds

X . i = Y . i;

compatibility redefine pred X = Y means :: PBOOLE:def 10

for i being object st i in I holds

X . i = Y . i;

( X = Y iff for i being object st i in I holds

X . i = Y . i ) by Th3;

:: deftheorem defines = PBOOLE:def 10 :

for I being set

for X, Y being ManySortedSet of I holds

( X = Y iff for i being object st i in I holds

X . i = Y . i );

for I being set

for X, Y being ManySortedSet of I holds

( X = Y iff for i being object st i in I holds

X . i = Y . i );

theorem 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

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

X (\/) Z c= Y (\/) V

proof end;

theorem :: PBOOLE:21

for I being set

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

X (/\) Z c= Y (/\) V

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

X (/\) Z c= Y (/\) V

proof end;

theorem :: PBOOLE:25

for I being set

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

X (\/) (Y (/\) Z) = (X (\/) Y) (/\) Z

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

X (\/) (Y (/\) Z) = (X (\/) Y) (/\) Z

proof end;

theorem :: PBOOLE:26

for I being set

for X, Y, Z being ManySortedSet of I holds

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

X c= V ) ) )

for X, Y, Z being ManySortedSet of I holds

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

X c= V ) ) )

proof end;

theorem :: PBOOLE:27

for I being set

for X, Y, Z being ManySortedSet of I holds

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

V c= X ) ) )

for X, Y, Z being ManySortedSet of I holds

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

V c= X ) ) )

proof end;

theorem Th32: :: PBOOLE:32

for I being set

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

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

proof end;

theorem Th33: :: PBOOLE:33

for I being set

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

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

proof end;

theorem :: PBOOLE:34

for I being set

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

X c= Y (\/) Z

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

X c= Y (\/) Z

proof end;

theorem :: PBOOLE:35

for I being set

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

Y (/\) Z c= X

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

Y (/\) Z c= X

proof end;

theorem :: PBOOLE:36

for I being set

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

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

proof end;

theorem :: PBOOLE:39

for I being set

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

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

proof end;

theorem :: PBOOLE:40

for I being set

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

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

proof end;

theorem :: PBOOLE:45

theorem :: PBOOLE:46

theorem :: PBOOLE:47

theorem :: PBOOLE:48

theorem :: PBOOLE:49

theorem :: PBOOLE:50

for I being set

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

X c= Y

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

X c= Y

proof end;

theorem :: PBOOLE:51

theorem :: PBOOLE:58

theorem :: PBOOLE:61

theorem Th64: :: PBOOLE:64

for I being set

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

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

proof end;

theorem Th69: :: PBOOLE:69

for I being set

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

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

proof end;

theorem Th72: :: PBOOLE:72

for I being set

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

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

proof end;

theorem :: PBOOLE:74

for I being set

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

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

proof end;

theorem :: PBOOLE:76

for I being set

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

( X (\) Y c= Z & X (\) Z c= Y )

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

( X (\) Y c= Z & X (\) Z c= Y )

proof end;

theorem Th77: :: PBOOLE:77

for I being set

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

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

proof end;

theorem :: PBOOLE:79

for I being set

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

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

proof end;

theorem :: PBOOLE:81

for I being set

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

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

proof end;

theorem :: PBOOLE:83

theorem :: PBOOLE:85

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

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

proof end;

theorem :: PBOOLE:89

for I being set

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

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

proof end;

theorem Th90: :: PBOOLE:90

for I being set

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

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

proof end;

theorem :: PBOOLE:91

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

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

X overlaps Y (\/) Z

proof end;

theorem Th101: :: PBOOLE:101

for I being set

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

Y overlaps V

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

Y overlaps V

proof end;

theorem :: PBOOLE:102

for I being set

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

( X overlaps Y & X overlaps Z )

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

( X overlaps Y & X overlaps Z )

proof end;

theorem :: PBOOLE:103

for I being set

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

X overlaps Z (/\) V

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

X overlaps Z (/\) V

proof end;

theorem :: PBOOLE:104

theorem :: PBOOLE:105

for I being set

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

not X (/\) Y overlaps X (/\) Z

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

not X (/\) Y overlaps X (/\) Z

proof end;

theorem :: PBOOLE:113

for I being set

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

X = EmptyMS I

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

X = EmptyMS I

proof end;

theorem :: PBOOLE:114

for I being set

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

( X = V & Y = Z )

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

( X = V & Y = Z )

proof end;

definition

let I be set ;

let X, Y be ManySortedSet of I;

reflexivity

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

x in X ;

end;
let X, Y be ManySortedSet of I;

reflexivity

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

x in X ;

:: deftheorem defines [= PBOOLE:def 11 :

for I being set

for X, Y being ManySortedSet of I holds

( X [= Y iff for x being ManySortedSet of I st x in X holds

x in Y );

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

theorem :: PBOOLE:125

theorem Th127: :: PBOOLE:127

for I being non empty set

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

not X overlaps Y

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

not X overlaps Y

proof end;

definition

let I be set ;

let X be ManySortedSet of I;

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

X . i is empty )

( X is non-empty iff for i being object st i in I holds

not X . i is empty )

end;
let X be ManySortedSet of I;

:: original: empty-yielding

redefine attr X is empty-yielding means :: PBOOLE:def 12

for i being object st i in I holds

X . i is empty ;

compatibility redefine attr X is empty-yielding means :: PBOOLE:def 12

for i being object st i in I holds

X . i is empty ;

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

X . i is empty )

proof end;

:: original: non-empty

redefine attr X is non-empty means :Def13: :: PBOOLE:def 13

for i being object st i in I holds

not X . i is empty ;

compatibility redefine attr X is non-empty means :Def13: :: PBOOLE:def 13

for i being object st i in I holds

not X . i is empty ;

( X is non-empty iff for i being object st i in I holds

not X . i is empty )

proof end;

:: deftheorem defines empty-yielding PBOOLE:def 12 :

for I being set

for X being ManySortedSet of I holds

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

X . i is empty );

for I being set

for X being ManySortedSet of I holds

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

X . i is empty );

:: deftheorem Def13 defines non-empty PBOOLE:def 13 :

for I being set

for X being ManySortedSet of I holds

( X is non-empty iff for i being object st i in I holds

not X . i is empty );

for I being set

for X being ManySortedSet of I holds

( X is non-empty iff for i being object st i in I holds

not X . i is empty );

registration

let I be set ;

existence

not for b_{1} being ManySortedSet of I holds b_{1} is V9()

not for b_{1} being ManySortedSet of I holds b_{1} is V8()

end;
existence

not for b

proof end;

existence not for b

proof end;

registration

let I be non empty set ;

coherence

for b_{1} being ManySortedSet of I st b_{1} is V8() holds

not b_{1} is V9()

for b_{1} being ManySortedSet of I st b_{1} is V9() holds

not b_{1} is V8()
;

end;
coherence

for b

not b

proof end;

coherence for b

not b

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

for Y being ManySortedSet of I

for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds

( x in X iff x in Y ) ) holds

X = Y

proof end;

theorem :: PBOOLE:136

for I being set

for Y, Z being ManySortedSet of I

for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds

( x in X iff ( x in Y & x in Z ) ) ) holds

X = Y (/\) Z

for Y, Z being ManySortedSet of I

for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds

( x in X iff ( x in Y & x in Z ) ) ) holds

X = Y (/\) Z

proof end;

registration
end;

theorem :: PBOOLE:138

for I being non empty set

for M being ManySortedSet of I

for A being Component of M ex i being object st

( i in I & A = M . i )

for M being ManySortedSet of I

for A being Component of M ex i being object st

( i in I & A = M . i )

proof end;

theorem :: PBOOLE:139

for I being set

for M being ManySortedSet of I

for i being object st i in I holds

M . i is Component of M

for M being ManySortedSet of I

for i being object st i in I holds

M . i is Component of M

proof end;

definition

let I be set ;

let B be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i is Element of B . i

end;
let B be ManySortedSet of I;

mode Element of B -> ManySortedSet of I means :: PBOOLE:def 14

for i being object st i in I holds

it . i is Element of B . i;

existence for i being object st i in I holds

it . i is Element of B . i;

ex b

for i being object st i in I holds

b

proof end;

:: deftheorem defines Element PBOOLE:def 14 :

for I being set

for B, b_{3} being ManySortedSet of I holds

( b_{3} is Element of B iff for i being object st i in I holds

b_{3} . i is Element of B . i );

for I being set

for B, b

( b

b

definition

let I be set ;

let A, B be ManySortedSet of I;

existence

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i is Function of (A . i),(B . i);

end;
let A, B be ManySortedSet of I;

mode ManySortedFunction of A,B -> ManySortedSet of I means :Def15: :: PBOOLE:def 15

for i being object st i in I holds

it . i is Function of (A . i),(B . i);

correctness for i being object st i in I holds

it . i is Function of (A . i),(B . i);

existence

ex b

for i being object st i in I holds

b

proof end;

:: deftheorem Def15 defines ManySortedFunction PBOOLE:def 15 :

for I being set

for A, B, b_{4} being ManySortedSet of I holds

( b_{4} is ManySortedFunction of A,B iff for i being object st i in I holds

b_{4} . i is Function of (A . i),(B . i) );

for I being set

for A, B, b

( b

b

registration

let I be set ;

let A, B be ManySortedSet of I;

coherence

for b_{1} being ManySortedFunction of A,B holds b_{1} is Function-yielding

end;
let A, B be ManySortedSet of I;

coherence

for b

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

coherence

for b_{1} being I -defined Function st b_{1} = F * O holds

b_{1} is total

end;
let J be non empty set ;

let O be Function of I,J;

let F be ManySortedSet of J;

coherence

for b

b

proof end;

registration

let J be non empty set ;

let B be V8() ManySortedSet of J;

let j be Element of J;

coherence

not B . j is empty by Def13;

end;
let B be V8() ManySortedSet of J;

let j be Element of J;

coherence

not B . j is empty by Def13;

definition

let I be set ;

let X, Y be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = [:(X . i),(Y . i):]

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = [:(X . i),(Y . i):] ) & ( for i being object st i in I holds

b_{2} . i = [:(X . i),(Y . i):] ) holds

b_{1} = b_{2}

end;
let X, Y be ManySortedSet of I;

func [|X,Y|] -> ManySortedSet of I means :: PBOOLE:def 16

for i being object st i in I holds

it . i = [:(X . i),(Y . i):];

existence for i being object st i in I holds

it . i = [:(X . i),(Y . i):];

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines [| PBOOLE:def 16 :

for I being set

for X, Y, b_{4} being ManySortedSet of I holds

( b_{4} = [|X,Y|] iff for i being object st i in I holds

b_{4} . i = [:(X . i),(Y . i):] );

for I being set

for X, Y, b

( b

b

definition

let I be set ;

let X, Y be ManySortedSet of I;

deffunc H_{1}( object ) -> set = Funcs ((X . $1),(Y . $1));

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = Funcs ((X . i),(Y . i))

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = Funcs ((X . i),(Y . i)) ) & ( for i being object st i in I holds

b_{2} . i = Funcs ((X . i),(Y . i)) ) holds

b_{1} = b_{2}

end;
let X, Y be ManySortedSet of I;

deffunc H

func (Funcs) (X,Y) -> ManySortedSet of I means :: PBOOLE:def 17

for i being object st i in I holds

it . i = Funcs ((X . i),(Y . i));

existence for i being object st i in I holds

it . i = Funcs ((X . i),(Y . i));

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines (Funcs) PBOOLE:def 17 :

for I being set

for X, Y, b_{4} being ManySortedSet of I holds

( b_{4} = (Funcs) (X,Y) iff for i being object st i in I holds

b_{4} . i = Funcs ((X . i),(Y . i)) );

for I being set

for X, Y, b

( b

b

definition

let I be set ;

let M be ManySortedSet of I;

existence

ex b_{1} being ManySortedSet of I st b_{1} c= M
;

end;
let M be ManySortedSet of I;

existence

ex b

:: deftheorem Def18 defines ManySortedSubset PBOOLE:def 18 :

for I being set

for M, b_{3} being ManySortedSet of I holds

( b_{3} is ManySortedSubset of M iff b_{3} c= M );

for I being set

for M, b

( b

registration

let I be set ;

let M be V8() ManySortedSet of I;

existence

not for b_{1} being ManySortedSubset of M holds b_{1} is V8()

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

existence

not for b

proof end;

definition

let F, G be Function-yielding Function;

ex b_{1} being Function st

( dom b_{1} = (dom F) /\ (dom G) & ( for i being object st i in dom b_{1} holds

b_{1} . i = (G . i) * (F . i) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom F) /\ (dom G) & ( for i being object st i in dom b_{1} holds

b_{1} . i = (G . i) * (F . i) ) & dom b_{2} = (dom F) /\ (dom G) & ( for i being object st i in dom b_{2} holds

b_{2} . i = (G . i) * (F . i) ) holds

b_{1} = b_{2}

end;
func G ** F -> Function means :Def19: :: PBOOLE:def 19

( dom it = (dom F) /\ (dom G) & ( for i being object st i in dom it holds

it . i = (G . i) * (F . i) ) );

existence ( dom it = (dom F) /\ (dom G) & ( for i being object st i in dom it holds

it . i = (G . i) * (F . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def19 defines ** PBOOLE:def 19 :

for F, G being Function-yielding Function

for b_{3} being Function holds

( b_{3} = G ** F iff ( dom b_{3} = (dom F) /\ (dom G) & ( for i being object st i in dom b_{3} holds

b_{3} . i = (G . i) * (F . i) ) ) );

for F, G being Function-yielding Function

for b

( b

b

registration
end;

definition

let I be set ;

let A be ManySortedSet of I;

let F be ManySortedFunction of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i = (F . i) .: (A . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being set st i in I holds

b_{1} . i = (F . i) .: (A . i) ) & ( for i being set st i in I holds

b_{2} . i = (F . i) .: (A . i) ) holds

b_{1} = b_{2}

end;
let A be ManySortedSet of I;

let F be ManySortedFunction of I;

func F .:.: A -> ManySortedSet of I means :: PBOOLE:def 20

for i being set st i in I holds

it . i = (F . i) .: (A . i);

existence for i being set st i in I holds

it . i = (F . i) .: (A . i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines .:.: PBOOLE:def 20 :

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I

for b_{4} being ManySortedSet of I holds

( b_{4} = F .:.: A iff for i being set st i in I holds

b_{4} . i = (F . i) .: (A . i) );

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I

for b

( b

b

registration
end;

registration

let A be non empty set ;

coherence

for b_{1} being ManySortedSet of A st b_{1} is V8() holds

not b_{1} is V9()
;

end;
coherence

for b

not b

registration
end;

registration

let I be set ;

let f be V8() ManySortedSet of I;

existence

ex b_{1} being I -defined f -compatible Function st b_{1} is total

end;
let f be V8() ManySortedSet of I;

existence

ex b

proof end;

theorem :: PBOOLE:141

for I being set

for f being V8() ManySortedSet of I

for p being b_{1} -defined b_{2} -compatible Function ex s being b_{2} -compatible ManySortedSet of I st p c= s

for f being V8() ManySortedSet of I

for p being b

proof end;

registration

let X be non empty set ;

let Y be set ;

existence

ex b_{1} being ManySortedSet of Y st b_{1} is X -valued

end;
let Y be set ;

existence

ex b

proof end;

theorem :: PBOOLE:143

for I, Y being non empty set

for M being b_{2} -valued ManySortedSet of I

for x being Element of I holds M . x = M /. x

for M being b

for x being Element of I holds M . x = M /. x

proof end;

theorem :: PBOOLE:145

for I being set

for Y being non empty set

for p being b_{1} -defined b_{2} -valued Function ex s being b_{2} -valued ManySortedSet of I st p c= s

for Y being non empty set

for p being b

proof end;

theorem :: PBOOLE:146

definition

let I be non empty set ;

let A, B be ManySortedSet of I;

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

end;
let A, B be ManySortedSet of I;

:: original: =

redefine pred A = B means :: PBOOLE:def 21

for i being Element of I holds A . i = B . i;

compatibility redefine pred A = B means :: PBOOLE:def 21

for i being Element of I holds A . i = B . i;

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

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

for I being non empty set

for A, B being ManySortedSet of I holds

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

registration
end;