COH_SP

:: COH_SP semantic presentation

begin

definition

let IT be ( ( ) ( ) set ) ;

attr IT is binary_complete means :: COH_SP:def 1
for A being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= IT : ( ( ) ( ) CatStr ) & ( for a, b being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
a : ( ( ) ( ) set ) \/ b : ( ( ) ( ) set ) : ( ( ) ( ) set ) in IT : ( ( ) ( ) CatStr ) ) holds
union A : ( ( ) ( ) set ) : ( ( ) ( ) set ) in IT : ( ( ) ( ) CatStr ) ;

end;

registration

cluster non empty subset-closed binary_complete for ( ( ) ( ) set ) ;

end;

definition

mode Coherence_Space is ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) set ) ;

end;

theorem :: COH_SP:1

for C being ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) holds {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) in C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ;

theorem :: COH_SP:2

for X being ( ( ) ( ) set ) holds bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ;

theorem :: COH_SP:3

{{} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) } : ( ( ) ( functional non empty ) set ) is ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ;

theorem :: COH_SP:4

for x being ( ( ) ( ) set )
for C being ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) st x : ( ( ) ( ) set ) in union C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ;

definition

let C be ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ;

func Web C -> ( ( total V27() V29() ) ( Relation-like union C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined union C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) means :: COH_SP:def 2
for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in it : ( ( ) ( ) set ) iff ex X being ( ( ) ( ) set ) st
( X : ( ( ) ( ) set ) in C : ( ( ) ( ) CatStr ) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) );

end;

theorem :: COH_SP:5

theorem :: COH_SP:6

theorem :: COH_SP:7

for a being ( ( ) ( ) set )
for C being ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) holds
( a : ( ( ) ( ) set ) in C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) holds
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in Web C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( total V27() V29() ) ( Relation-like union b₂ : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) -defined union b₂ : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ;

theorem :: COH_SP:8

for a being ( ( ) ( ) set )
for C being ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) st ( for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) holds
{x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) ) holds
a : ( ( ) ( ) set ) c= union C : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) ;

theorem :: COH_SP:9

theorem :: COH_SP:10

theorem :: COH_SP:11

definition

let X be ( ( ) ( ) set ) ;
let E be ( ( total V27() V29() ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ;

func CohSp E -> ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) means :: COH_SP:def 3
for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) in it : ( ( Function-like quasi_total ) ( Relation-like E : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of bool [:E : ( ( ) ( ) set ) ,X : ( ( ) ( ) CatStr ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in a : ( ( ) ( ) set ) holds
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in E : ( ( ) ( ) set ) );

end;

theorem :: COH_SP:12

for X being ( ( ) ( ) set )
for E being ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds Web (CohSp E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( total V27() V29() ) ( Relation-like union (CohSp b₂ : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) -defined union (CohSp b₂ : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) = E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ;

theorem :: COH_SP:13

theorem :: COH_SP:14

for X, a being ( ( ) ( ) set )
for E being ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds
( a : ( ( ) ( ) set ) in CohSp E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) iff a : ( ( ) ( ) set ) is ( ( ) ( ) TolSet of E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ) ;

theorem :: COH_SP:15

for X being ( ( ) ( ) set )
for E being ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds CohSp E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) : ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) = TolSets E : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) : ( ( ) ( ) set ) ;

begin

definition

let X be ( ( ) ( ) set ) ;

func CSp X -> ( ( ) ( ) set ) equals :: COH_SP:def 4
{ x : ( ( ) ( ) Subset-Family of ) where x is ( ( ) ( ) Subset-Family of ) : x : ( ( ) ( ) Subset-Family of ) is ( ( non empty subset-closed binary_complete ) ( non empty subset-closed binary_complete ) Coherence_Space) } ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster CSp X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster -> non empty subset-closed binary_complete for ( ( ) ( ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: COH_SP:16

for X, x, y being ( ( ) ( ) set )
for C being ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in union C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in union C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

definition

let X be ( ( ) ( ) set ) ;

func FuncsC X -> ( ( ) ( ) set ) equals :: COH_SP:def 5
union { (Funcs ((union x : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(union y : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) where x, y is ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : verum } : ( ( ) ( ) set ) ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster FuncsC X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> functional non empty ;

end;

theorem :: COH_SP:17

for x, X being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) iff ex C1, C2 being ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st
( ( union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & x : ( ( ) ( ) set ) is ( ( Function-like quasi_total ) ( Relation-like union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₄ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;

func MapsC X -> ( ( ) ( ) set ) equals :: COH_SP:def 6
{ [[C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,CC : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,f : ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ] : ( ( ) ( V15() ) set ) where C, CC is ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , f is ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) : ( ( union CC : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies union C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & f : ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like union b₁ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union CC : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & ( for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
{(f : ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(f : ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in CC : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) } ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster MapsC X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: COH_SP:18

for X being ( ( ) ( ) set )
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ex g being ( ( ) ( Relation-like Function-like ) Element of FuncsC X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ex C1, C2 being ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st
( l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [[C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,g : ( ( ) ( Relation-like Function-like ) Element of FuncsC b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ] : ( ( ) ( V15() ) set ) & ( union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & g : ( ( ) ( Relation-like Function-like ) Element of FuncsC b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like union b₄ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₅ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & ( for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
{(g : ( ( ) ( Relation-like Function-like ) Element of FuncsC b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(g : ( ( ) ( Relation-like Function-like ) Element of FuncsC b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: COH_SP:19

for X being ( ( ) ( ) set )
for C1, C2 being ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) st ( union C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies union C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & ( for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
{(f : ( ( Function-like quasi_total ) ( Relation-like union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(f : ( ( Function-like quasi_total ) ( Relation-like union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
[[C1 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,C2 : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,f : ( ( Function-like quasi_total ) ( Relation-like union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union b₃ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ] : ( ( ) ( V15() ) set ) in MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

registration

let X be ( ( ) ( ) set ) ;
let l be ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

cluster l : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -> Relation-like Function-like ;

end;

definition

let X be ( ( ) ( ) set ) ;
let l be ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func dom l -> ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 7
(l : ( ( ) ( ) set ) `1) : ( ( ) ( ) set ) `1 : ( ( ) ( ) set ) ;

func cod l -> ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 8
(l : ( ( ) ( ) set ) `1) : ( ( ) ( ) set ) `2 : ( ( ) ( ) set ) ;

end;

theorem :: COH_SP:20

for X being ( ( ) ( ) set )
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [[(dom l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(cod l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,(l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) ] : ( ( ) ( V15() ) set ) ;

definition

let X be ( ( ) ( ) set ) ;
let C be ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func id$ C -> ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 9
[[C : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) ,(id (union C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( total ) ( Relation-like union C : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined union C : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:(union C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(union C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ;

end;

theorem :: COH_SP:21

for X being ( ( ) ( ) set )
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( ( union (cod l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) or union (dom l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like union (dom b₂ : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union (cod b₂ : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of union (dom l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , union (cod l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & ( for x, y being ( ( ) ( ) set ) st {x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in dom l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
{((l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,((l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) in cod l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;
let l1, l2 be ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
assume cod l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func l2 * l1 -> ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 10
[[(dom l1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(cod l2 : ( ( Function-like quasi_total ) ( Relation-like l1 : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:l1 : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,((l2 : ( ( Function-like quasi_total ) ( Relation-like l1 : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:l1 : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) set ) * (l1 : ( ( ) ( ) set ) `2) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ] : ( ( ) ( V15() ) set ) ;

end;

theorem :: COH_SP:22

for X being ( ( ) ( ) set )
for l2, l1 being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( (l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) = (l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) * (l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) & dom (l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & cod (l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: COH_SP:23

for X being ( ( ) ( ) set )
for l2, l1, l3 being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & dom l3 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
l3 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * (l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (l3 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l2 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: COH_SP:24

for X being ( ( ) ( ) set )
for C being ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( (id$ C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) = id (union C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( total ) ( Relation-like union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:(union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(union b₂ : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & dom (id$ C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & cod (id$ C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = C : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: COH_SP:25

for X being ( ( ) ( ) set )
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * (id$ (dom l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & (id$ (cod l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = l : ( ( ) ( ) Element of MapsC b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;

func CDom X -> ( ( Function-like quasi_total ) ( Relation-like MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) means :: COH_SP:def 11
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . l : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom l : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func CCod X -> ( ( Function-like quasi_total ) ( Relation-like MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) means :: COH_SP:def 12
for l being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . l : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func CComp X -> ( ( Function-like ) ( Relation-like [:(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) means :: COH_SP:def 13
( ( for l2, l1 being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( [l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) in dom it : ( ( ) ( ) set ) : ( ( ) ( Relation-like MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [:(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) iff dom l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for l2, l1 being ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty subset-closed binary_complete ) Element of CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
it : ( ( ) ( ) set ) . [l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) = l2 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * l1 : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) );

end;

theorem :: COH_SP:26

canceled;

definition

canceled;
let X be ( ( ) ( ) set ) ;

func CohCat X -> ( ( non empty non void strict ) ( non empty non void strict ) CatStr ) equals :: COH_SP:def 15
CatStr(# (CSp X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(CDom X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(CCod X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , CSp X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(CComp X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like [:(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsC X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined MapsC X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) #) : ( ( strict ) ( non empty non void strict ) CatStr ) ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster CohCat X : ( ( ) ( ) set ) : ( ( non empty non void strict ) ( non empty non void strict ) CatStr ) -> non empty non void strict Category-like transitive associative reflexive ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster CohCat X : ( ( ) ( ) set ) : ( ( non empty non void strict ) ( non empty non void strict Category-like transitive associative reflexive ) CatStr ) -> non empty non void strict with_identities ;

end;

begin

definition

let X be ( ( ) ( ) set ) ;

func Toler X -> ( ( ) ( ) set ) means :: COH_SP:def 16
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff x : ( ( ) ( ) set ) is ( ( total V27() V29() ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) );

end;

registration

let X be ( ( ) ( ) set ) ;

cluster Toler X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

definition

let X be ( ( ) ( ) set ) ;

func Toler_on_subsets X -> ( ( ) ( ) set ) equals :: COH_SP:def 17
union { (Toler Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) where Y is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : verum } : ( ( ) ( ) set ) ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: COH_SP:27

for x, X being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) iff ex A being ( ( ) ( ) set ) st
( A : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) is ( ( total V27() V29() ) ( Relation-like b₃ : ( ( ) ( ) set ) -defined b₃ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ) ;

theorem :: COH_SP:28

for a being ( ( ) ( ) set ) holds Total a : ( ( ) ( ) set ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in Toler a : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:29

for X being ( ( ) ( ) set ) holds {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:30

for a, X being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
Total a : ( ( ) ( ) set ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:31

for a, X being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
id a : ( ( ) ( ) set ) : ( ( total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:32

for X being ( ( ) ( ) set ) holds Total X : ( ( ) ( ) set ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:33

for X being ( ( ) ( ) set ) holds id X : ( ( ) ( ) set ) : ( ( total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

definition

let X be ( ( ) ( ) set ) ;

func TOL X -> ( ( ) ( ) set ) equals :: COH_SP:def 18
{ [t : ( ( ) ( ) Element of Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) where t is ( ( ) ( ) Element of Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , Y is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : t : ( ( ) ( ) Element of Toler_on_subsets X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( total V27() V29() ) ( Relation-like b₂ : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued total quasi_total V27() V29() ) Tolerance of ) } ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster TOL X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: COH_SP:34

for X being ( ( ) ( ) set ) holds [{} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ] : ( ( ) ( V15() ) set ) in TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:35

for a, X being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
[(id a : ( ( ) ( ) set ) ) : ( ( total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:36

for a, X being ( ( ) ( ) set ) st a : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
[(Total a : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:37

for X being ( ( ) ( ) set ) holds [(id X : ( ( ) ( ) set ) ) : ( ( total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

theorem :: COH_SP:38

for X being ( ( ) ( ) set ) holds [(Total X : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued total quasi_total V27() V29() V34() ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₁ : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

definition

let X be ( ( ) ( ) set ) ;
let T be ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
:: original: `2
redefine func T `2 -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: `1
redefine func T `1 -> ( ( total V27() V29() ) ( Relation-like T : ( ( ) ( ) set ) `2 : ( ( ) ( ) set ) -defined T : ( ( ) ( ) set ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ;

end;

definition

let X be ( ( ) ( ) set ) ;

func FuncsT X -> ( ( ) ( ) set ) equals :: COH_SP:def 19
union { (Funcs ((T : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(TT : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( functional ) set ) where T, TT is ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : verum } : ( ( ) ( ) set ) ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster FuncsT X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> functional non empty ;

end;

theorem :: COH_SP:39

for x, X being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) iff ex T1, T2 being ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st
( ( T2 : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies T1 : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & x : ( ( ) ( ) set ) is ( ( Function-like quasi_total ) ( Relation-like b₃ : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₄ : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of T1 : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,T2 : ( ( ) ( ) Element of TOL b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;

func MapsT X -> ( ( ) ( ) set ) equals :: COH_SP:def 20
{ [[T : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,TT : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,f : ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ] : ( ( ) ( V15() ) set ) where T, TT is ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , f is ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) : ( ( TT : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies T : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & f : ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of T : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,TT : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) & ( for x, y being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in T : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₁ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds
[(f : ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(f : ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in TT : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ) } ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster MapsT X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

theorem :: COH_SP:40

for X being ( ( ) ( ) set )
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ex f being ( ( ) ( Relation-like Function-like ) Element of FuncsT X : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ex T1, T2 being ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st
( m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [[T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,f : ( ( ) ( Relation-like Function-like ) Element of FuncsT b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) ] : ( ( ) ( V15() ) set ) & ( T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & f : ( ( ) ( Relation-like Function-like ) Element of FuncsT b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like b₄ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₅ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) & ( for x, y being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₄ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₄ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds
[(f : ( ( ) ( Relation-like Function-like ) Element of FuncsT b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(f : ( ( ) ( Relation-like Function-like ) Element of FuncsT b₁ : ( ( ) ( ) set ) : ( ( ) ( functional non empty ) set ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₅ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₅ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ) ;

theorem :: COH_SP:41

for X being ( ( ) ( ) set )
for T1, T2 being ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) st ( T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) implies T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & ( for x, y being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds
[(f : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(f : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) holds
[[T1 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,T2 : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,f : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,b₃ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( V15() ) set ) in MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ;

registration

let X be ( ( ) ( ) set ) ;
let m be ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

cluster m : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -> Relation-like Function-like ;

end;

definition

let X be ( ( ) ( ) set ) ;
let m be ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func dom m -> ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 21
(m : ( ( ) ( ) set ) `1) : ( ( ) ( ) set ) `1 : ( ( ) ( ) set ) ;

func cod m -> ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 22
(m : ( ( ) ( ) set ) `1) : ( ( ) ( ) set ) `2 : ( ( ) ( ) set ) ;

end;

theorem :: COH_SP:42

for X being ( ( ) ( ) set )
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [[(dom m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(cod m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,(m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) ] : ( ( ) ( V15() ) set ) ;

definition

let X be ( ( ) ( ) set ) ;
let T be ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func id$ T -> ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 23
[[T : ( ( ) ( ) set ) ,T : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) ,(id (T : ( ( ) ( ) set ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( total ) ( Relation-like T : ( ( ) ( ) set ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined T : ( ( ) ( ) set ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:(T : ( ( ) ( ) set ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(T : ( ( ) ( ) set ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ;

end;

theorem :: COH_SP:43

for X being ( ( ) ( ) set )
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( ( (cod m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) or (dom m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty ) set ) ) & m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like (dom b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined (cod b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like quasi_total ) Function of (dom m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(cod m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) & ( for x, y being ( ( ) ( ) set ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in (dom m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like (dom b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined (dom b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) holds
[((m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,((m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) . y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) set ) in (cod m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `1 : ( ( total V27() V29() ) ( Relation-like (cod b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -defined (cod b₂ : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) -valued total quasi_total V27() V29() ) Tolerance of ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;
let m1, m2 be ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
assume cod m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func m2 * m1 -> ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) equals :: COH_SP:def 24
[[(dom m1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(cod m2 : ( ( Function-like quasi_total ) ( Relation-like m1 : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:m1 : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) ,((m2 : ( ( Function-like quasi_total ) ( Relation-like m1 : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:m1 : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) set ) * (m1 : ( ( ) ( ) set ) `2) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ] : ( ( ) ( V15() ) set ) ;

end;

theorem :: COH_SP:44

for X being ( ( ) ( ) set )
for m2, m1 being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( (m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) = (m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) * (m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( Relation-like Function-like ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) & dom (m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & cod (m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: COH_SP:45

for X being ( ( ) ( ) set )
for m2, m1, m3 being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & dom m3 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
m3 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * (m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (m3 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m2 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: COH_SP:46

for X being ( ( ) ( ) set )
for T being ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( (id$ T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( Relation-like Function-like ) set ) = id (T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( total ) ( Relation-like b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() ) Element of bool [:(b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(b₂ : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & dom (id$ T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & cod (id$ T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = T : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: COH_SP:47

for X being ( ( ) ( ) set )
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * (id$ (dom m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & (id$ (cod m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of TOL b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = m : ( ( ) ( ) Element of MapsT b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition

let X be ( ( ) ( ) set ) ;

func fDom X -> ( ( Function-like quasi_total ) ( Relation-like MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) means :: COH_SP:def 25
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . m : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom m : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func fCod X -> ( ( Function-like quasi_total ) ( Relation-like MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) means :: COH_SP:def 26
for m being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . m : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

func fComp X -> ( ( Function-like ) ( Relation-like [:(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) means :: COH_SP:def 27
( ( for m2, m1 being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
( [m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) in dom it : ( ( ) ( ) set ) : ( ( ) ( Relation-like MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [:(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) iff dom m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for m2, m1 being ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) st dom m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = cod m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
it : ( ( ) ( ) set ) . [m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V15() ) set ) : ( ( ) ( ) set ) = m2 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * m1 : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) );

end;

definition

canceled;
let X be ( ( ) ( ) set ) ;

func TolCat X -> ( ( non empty non void strict ) ( non empty non void strict ) CatStr ) equals :: COH_SP:def 29
CatStr(# (TOL X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(fDom X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(fCod X : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -defined TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) , TOL X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(fComp X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like [:(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(MapsT X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined MapsT X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) #) : ( ( strict ) ( non empty non void strict ) CatStr ) ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster TolCat X : ( ( ) ( ) set ) : ( ( non empty non void strict ) ( non empty non void strict ) CatStr ) -> non empty non void strict Category-like transitive associative reflexive ;

end;

registration

let X be ( ( ) ( ) set ) ;

cluster TolCat X : ( ( ) ( ) set ) : ( ( non empty non void strict ) ( non empty non void strict Category-like transitive associative reflexive ) CatStr ) -> non empty non void strict with_identities ;

end;