:: Equivalence Relations and Classes of Abstraction
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

:: Equivalence Relation and its properties
definition
let X be set ;
func nabla X ->  Relation of X equals :: EQREL_1:def 1
[:X,X:];
coherence
 [:X,X:] is Relation of X
proofend;
end;

:: deftheorem  defines nabla EQREL_1:def_1_:_
 for X being set holds nabla X = [:X,X:];

registration
let X be set ;
cluster nabla X ->  reflexive total ;
coherence
 ( nabla X is total & nabla X is reflexive )
proofend;
end;

definition
let X be set ;
let R1, R2 be Relation of X;
:: original:/\
redefine funcR1 /\ R2 ->  Relation of X;
coherence
 R1 /\ R2 is Relation of X
proofend;
:: original:\/
redefine funcR1 \/ R2 ->  Relation of X;
coherence
 R1 \/ R2 is Relation of X
proofend;
end;

theorem :: EQREL_1:1
for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X by XBOOLE_1:12;

theorem :: EQREL_1:2
for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
proofend;

definition
let X be set ;
mode Tolerance of X is reflexive symmetric total Relation of X;
mode Equivalence_Relation of X is symmetric transitive total Relation of X;
end;

theorem :: EQREL_1:3
for X being set holds id X is Equivalence_Relation of X ;

theorem Th4: :: EQREL_1:4
for X being set holds nabla X is Equivalence_Relation of X
proofend;

registration
let X be set ;
cluster nabla X ->  symmetric transitive total ;
coherence
 ( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;
end;

Lm1:  for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
proofend;

theorem Th5: :: EQREL_1:5
for X, x being set
for R being reflexive total Relation of X st x in X holds
[x,x] in R
proofend;

theorem Th6: :: EQREL_1:6
for X, x, y being set
for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
proofend;

theorem Th7: :: EQREL_1:7
for X, x, y, z being set
for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
proofend;

theorem :: EQREL_1:8
for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} ;

theorem Th9: :: EQREL_1:9
for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive &amp; R is symmetric &amp; R is transitive &amp; field R = X ) )
proofend;

definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
:: original:/\
redefine funcEqR1 /\ EqR2 ->  Equivalence_Relation of X;
coherence
 EqR1 /\ EqR2 is Equivalence_Relation of X
proofend;
end;

theorem :: EQREL_1:10
for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
proofend;

theorem Th11: :: EQREL_1:11
for X being set
for SFXX being Subset-Family of [:X,X:] st SFXX <> {} &amp; ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X
proofend;

theorem Th12: :: EQREL_1:12
for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR &amp; ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
proofend;

definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
funcEqR1 "\/" EqR2 ->  Equivalence_Relation of X means :Def2: :: EQREL_1:def 2
( EqR1 \/ EqR2 c= it &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
it c= EqR ) );
existence
 ex b1 being Equivalence_Relation of X st
( EqR1 \/ EqR2 c= b1 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) ) by Th12;
uniqueness
 for b1, b2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) &amp; EqR1 \/ EqR2 c= b2 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b2 c= EqR ) holds
b1 = b2
proofend;
commutativity
 for b1, EqR1, EqR2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) holds
( EqR2 \/ EqR1 c= b1 &amp; ( for EqR being Equivalence_Relation of X st EqR2 \/ EqR1 c= EqR holds
b1 c= EqR ) ) ;
idempotence
 for EqR1 being Equivalence_Relation of X holds
( EqR1 \/ EqR1 c= EqR1 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR1 c= EqR holds
EqR1 c= EqR ) ) ;
end;

:: deftheorem Def2 defines "\/" EQREL_1:def_2_:_
 for X being set
for EqR1, EqR2, b4 being Equivalence_Relation of X holds
( b4 = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b4 &amp; ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b4 c= EqR ) ) );

theorem :: EQREL_1:13
for X being set
for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proofend;

theorem :: EQREL_1:14
for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;

theorem :: EQREL_1:15
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqR2 "\/" EqR1 ;

theorem :: EQREL_1:16
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proofend;

theorem :: EQREL_1:17
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1
proofend;

scheme :: EQREL_1:sch 1
ExEqRel{ F1() ->  set , P1[ set , set ] } :
 ex EqR being Equivalence_Relation of F1() st
for x, y being set holds
( [x,y] in EqR iff ( x in F1() &amp; y in F1() &amp; P1[x,y] ) )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st P1[x,y] holds
P1[y,x] and
A3: for x, y, z being set st P1[x,y] &amp; P1[y,z] holds
P1[x,z]
proofend;

notation
let R be Relation;
let x be set ;
synonym  Class (R,x) for  Im (R,x);
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
:: original:Class
redefine func Class (R,x) ->  Subset of Y;
coherence
 Class (R,x) is Subset of Y
proofend;
end;

theorem :: EQREL_1:18
for y, x being set
for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
proofend;

theorem Th19: :: EQREL_1:19
for X, y, x being set
for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )
proofend;

theorem Th20: :: EQREL_1:20
for X being set
for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
proofend;

theorem :: EQREL_1:21
for X being set
for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)
proofend;

theorem :: EQREL_1:22
for X, y, x, z being set
for R being transitive Tolerance of X st y in Class (R,x) &amp; z in Class (R,x) holds
[y,z] in R
proofend;

Lm2:  for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
proofend;

theorem Th23: :: EQREL_1:23
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
proofend;

theorem Th24: :: EQREL_1:24
for X being set
for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
proofend;

theorem Th25: :: EQREL_1:25
for X, x being set st x in X holds
Class ((id X),x) = {x}
proofend;

theorem Th26: :: EQREL_1:26
for X, x being set st x in X holds
Class ((nabla X),x) = X
proofend;

theorem Th27: :: EQREL_1:27
for X being set
for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X
proofend;

theorem :: EQREL_1:28
for x, X, y being set
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f &amp; x = f . 1 &amp; y = f . (len f) &amp; ( for i being Element of NAT st 1 <= i &amp; i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
proofend;

theorem Th29: :: EQREL_1:29
for X being set
for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
proofend;

theorem :: EQREL_1:30
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
proofend;

definition
let X be set ;
let EqR be Equivalence_Relation of X;
func Class EqR ->  Subset-Family of X means :Def3: :: EQREL_1:def 3
 for A being Subset of X holds
( A in it iff ex x being set st
( x in X &amp; A = Class (EqR,x) ) );
existence
 ex b1 being Subset-Family of X st
for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X &amp; A = Class (EqR,x) ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of X st ( for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X &amp; A = Class (EqR,x) ) ) ) &amp; ( for A being Subset of X holds
( A in b2 iff ex x being set st
( x in X &amp; A = Class (EqR,x) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Class EQREL_1:def_3_:_
 for X being set
for EqR being Equivalence_Relation of X
for b3 being Subset-Family of X holds
( b3 = Class EqR iff for A being Subset of X holds
( A in b3 iff ex x being set st
( x in X &amp; A = Class (EqR,x) ) ) );

theorem Th31: :: EQREL_1:31
for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
proofend;

definition
let X be set ;
mode a_partition of X ->  Subset-Family of X means :Def4: :: EQREL_1:def 4
( union it = X &amp; ( for A being Subset of X st A in it holds
( A <> {} &amp; ( for B being Subset of X holds
( not B in it or A = B or A misses B ) ) ) ) );
existence
 ex b1 being Subset-Family of X st
( union b1 = X &amp; ( for A being Subset of X st A in b1 holds
( A <> {} &amp; ( for B being Subset of X holds
( not B in b1 or A = B or A misses B ) ) ) ) )
proofend;
end;

:: deftheorem Def4 defines a_partition EQREL_1:def_4_:_
 for X being set
for b2 being Subset-Family of X holds
( b2 is a_partition of X iff ( union b2 = X &amp; ( for A being Subset of X st A in b2 holds
( A <> {} &amp; ( for B being Subset of X holds
( not B in b2 or A = B or A misses B ) ) ) ) ) );

theorem Th32: :: EQREL_1:32
for P being a_partition of {} holds P = {}
proofend;

theorem Th33: :: EQREL_1:33
for X being set
for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X
proofend;

theorem Th34: :: EQREL_1:34
for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
proofend;

theorem :: EQREL_1:35
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) by Lm2;

theorem :: EQREL_1:36
for x, X being set
for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)
proofend;

begin

:: from FSM_1, PARTIT1, 2005.02.06, A.T.
registration
let X be non empty set ;
cluster  ->  non empty for a_partition of X;
coherence
 for b1 being a_partition of X holds not b1 is empty
proofend;
end;

:: from PUA2MSS1
registration
let X be set ;
cluster  ->  with_non-empty_elements for a_partition of X;
coherence
 for b1 being a_partition of X holds b1 is with_non-empty_elements
proofend;
end;

definition
let X be set ;
let R be Equivalence_Relation of X;
:: original:Class
redefine func Class R ->  a_partition of X;
coherence
 Class R is a_partition of X by Th33;
end;

:: from PRALG_3
registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R ->  non empty ;
coherence
 not Class R is empty ;
end;

registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R ->  with_non-empty_elements ;
coherence
 Class R is with_non-empty_elements ;
end;

notation
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
synonym  EqClass (R,x) for  Class (I,R);
end;

definition
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
:: original:Class
redefine func EqClass (R,x) ->  Element of Class R;
coherence
 Class (R,x) is Element of Class R
proofend;
end;

definition
let X be set ;
func SmallestPartition X ->  a_partition of X equals :: EQREL_1:def 5
 Class (id X);
coherence
 Class (id X) is a_partition of X ;
end;

:: deftheorem  defines SmallestPartition EQREL_1:def_5_:_
 for X being set holds SmallestPartition X = Class (id X);

theorem :: EQREL_1:37
for X being non empty set holds SmallestPartition X =  {  {x} where x is Element of X : verum  }
proofend;

definition
let X be non empty set ;
let x be Element of X;
let S1 be a_partition of X;
func EqClass (x,S1) ->  Subset of X means :Def6: :: EQREL_1:def 6
( x in it &amp; it in S1 );
existence
 ex b1 being Subset of X st
( x in b1 &amp; b1 in S1 )
proofend;
uniqueness
 for b1, b2 being Subset of X st x in b1 &amp; b1 in S1 &amp; x in b2 &amp; b2 in S1 holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines EqClass EQREL_1:def_6_:_
 for X being non empty set
for x being Element of X
for S1 being a_partition of X
for b4 being Subset of X holds
( b4 = EqClass (x,S1) iff ( x in b4 &amp; b4 in S1 ) );

theorem Th38: :: EQREL_1:38
for X being non empty set
for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds
S1 = S2
proofend;

theorem Th39: :: EQREL_1:39
for X being non empty set holds {X} is a_partition of X
proofend;

definition
let X be set ;
mode Family-Class of X is Subset-Family of (bool X);
end;

definition
let X be set ;
let F be Family-Class of X;
attrF is partition-membered  means :Def7: :: EQREL_1:def 7
 for S being set st S in F holds
S is a_partition of X;
end;

:: deftheorem Def7 defines partition-membered EQREL_1:def_7_:_
 for X being set
for F being Family-Class of X holds
( F is partition-membered iff for S being set st S in F holds
S is a_partition of X );

registration
let X be set ;
cluster partition-membered for Element of bool (bool (bool X));
existence
 ex b1 being Family-Class of X st b1 is partition-membered
proofend;
end;

definition
let X be set ;
mode Part-Family of X is partition-membered Family-Class of X;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
 not for b1 being a_partition of X holds b1 is empty
proofend;
end;

theorem Th40: :: EQREL_1:40
for X being set
for p being a_partition of X holds {p} is Part-Family of X
proofend;

registration
let X be set ;
cluster non empty partition-membered for Element of bool (bool (bool X));
existence
 not for b1 being Part-Family of X holds b1 is empty
proofend;
end;

theorem Th41: :: EQREL_1:41
for X being non empty set
for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
proofend;

Lm3:  for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
ex T being a_partition of X st
( T in F &amp; A = EqClass (x,T) )
proofend;

theorem :: EQREL_1:42
for A being set
for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
proofend;

definition
let X be non empty set ;
let F be non empty Part-Family of X;
func Intersection F ->  non empty a_partition of X means :: EQREL_1:def 8
 for x being Element of X holds EqClass (x,it) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
uniqueness
 for b1, b2 being non empty a_partition of X st ( for x being Element of X holds EqClass (x,b1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) &amp; ( for x being Element of X holds EqClass (x,b2) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) holds
b1 = b2
proofend;
existence
 ex b1 being non empty a_partition of X st
for x being Element of X holds EqClass (x,b1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
proofend;
end;

:: deftheorem  defines Intersection EQREL_1:def_8_:_
 for X being non empty set
for F being non empty Part-Family of X
for b3 being non empty a_partition of X holds
( b3 = Intersection F iff for x being Element of X holds EqClass (x,b3) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  );

theorem Th43: :: EQREL_1:43
for X being non empty set
for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
proofend;

theorem :: EQREL_1:44
for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
proofend;

:: Added 2007.10.17, AK
theorem :: EQREL_1:45
{} is a_partition of {}
proofend;

begin

theorem :: EQREL_1:46
for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1
proofend;

theorem Th47: :: EQREL_1:47
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e
proofend;

theorem Th48: :: EQREL_1:48
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
proofend;

theorem Th49: :: EQREL_1:49
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 &amp; (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
proofend;

theorem Th50: :: EQREL_1:50
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 &amp; (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
proofend;

theorem :: EQREL_1:51
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A &amp; ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
proofend;

theorem :: EQREL_1:52
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A &amp; ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
proofend;

theorem :: EQREL_1:53
for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
proofend;

theorem :: EQREL_1:54
for X being set
for a being Subset-Family of X holds union (union a) = union  {  (union A) where A is Subset of X : A in a  }
proofend;

theorem Th55: :: EQREL_1:55
for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
proofend;

theorem :: EQREL_1:56
for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
proofend;

theorem :: EQREL_1:57
for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
proofend;

theorem :: EQREL_1:58
for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
proofend;

theorem :: EQREL_1:59
for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
proofend;

theorem :: EQREL_1:60
for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
proofend;

theorem :: EQREL_1:61
for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
proofend;

theorem :: EQREL_1:62
for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
proofend;

theorem :: EQREL_1:63
for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
proofend;

theorem :: EQREL_1:64
for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
 not for b1 being a_partition of X holds b1 is empty
proofend;
end;

definition
let X be non empty set ;
let D be non empty a_partition of X;
func proj D ->  Function of X,D means :Def9: :: EQREL_1:def 9
 for p being Element of X holds p in it . p;
existence
 ex b1 being Function of X,D st
for p being Element of X holds p in b1 . p
proofend;
correctness
uniqueness
for b1, b2 being Function of X,D st ( for p being Element of X holds p in b1 . p ) &amp; ( for p being Element of X holds p in b2 . p ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def9 defines proj EQREL_1:def_9_:_
 for X being non empty set
for D being non empty a_partition of X
for b3 being Function of X,D holds
( b3 = proj D iff for p being Element of X holds p in b3 . p );

theorem Th65: :: EQREL_1:65
for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
proofend;

theorem :: EQREL_1:66
for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
proofend;

theorem :: EQREL_1:67
for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
proofend;

theorem :: EQREL_1:68
for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
proofend;

theorem :: EQREL_1:69
for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D &amp; B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
proofend;

theorem :: EQREL_1:70
for X being set
for P being a_partition of X
for x, a, b being set st x in a &amp; a in P &amp; x in b &amp; b in P holds
a = b
proofend;