begin
definition
let C be ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ;
func C opp -> ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict )
CatStr )
equals
CatStr(# the
carrier of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set ) , the
carrier' of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set ) , the
Target of
C : ( ( ) ( )
CatStr ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set )
-defined the
carrier of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [: the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) , the
Source of
C : ( ( ) ( )
CatStr ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set )
-defined the
carrier of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [: the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
(~ the Comp of C : ( ( ) ( ) CatStr ) : ( ( Function-like ) ( Relation-like [: the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:[: the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like ) (
Relation-like [: the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier' of
C : ( ( ) ( )
CatStr ) : ( ( ) ( )
set )
-valued Function-like )
PartFunc of ,) #) : ( (
strict ) (
strict )
CatStr ) ;
end;
theorem
for
C being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
a,
b,
c being ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) st
Hom (
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) &
Hom (
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) holds
for
f being ( ( ) ( )
Morphism of
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) ( )
Morphism of
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) holds
(g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) (*) f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( )
Element of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) )
= (f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
(*) (g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
C being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
a,
b,
c being ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) st
Hom (
(b : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) opp) : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
(a : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) opp) : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) &
Hom (
(c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) opp) : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
(b : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) opp) : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) holds
for
f being ( ( ) ( )
Morphism of
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) ( )
Morphism of
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) holds
(g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) (*) f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( )
Element of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) )
= (f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
(*) (g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
C being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
a,
b,
c being ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) ( )
Morphism of
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) ( )
Morphism of
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) st
Hom (
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) &
Hom (
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) holds
(g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) * f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( )
Morphism of
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
opp : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
= (f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
(*) (g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) ) ;
definition
let C,
D be ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ;
mode Contravariant_Functor of
C,
D -> ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set )
-defined the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) , the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
means
( ( for
c being ( ( ) ( )
Object of ( ( ) ( )
set ) ) ex
d being ( ( ) ( )
Object of ( ( ) ( )
set ) ) st
it : ( (
Function-like quasi_total ) (
Relation-like D : ( ( ) ( )
set )
-defined C : ( (
V36() ) (
V36() )
set )
-valued Function-like quasi_total )
Element of
bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. (id c : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Morphism of
b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) ,
b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= id d : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Morphism of
b2 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) ) ) & ( for
f being ( ( ) ( )
Morphism of ( ( ) ( )
set ) ) holds
(
it : ( (
Function-like quasi_total ) (
Relation-like D : ( ( ) ( )
set )
-defined C : ( (
V36() ) (
V36() )
set )
-valued Function-like quasi_total )
Element of
bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. (id (dom f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of C : ( ( V36() ) ( V36() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Morphism of
dom b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) ,
dom b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= id (cod (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Morphism of
cod (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
cod (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) &
it : ( (
Function-like quasi_total ) (
Relation-like D : ( ( ) ( )
set )
-defined C : ( (
V36() ) (
V36() )
set )
-valued Function-like quasi_total )
Element of
bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. (id (cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of C : ( ( V36() ) ( V36() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Morphism of
cod b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) ,
cod b1 : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= id (dom (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Morphism of
dom (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
dom (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) ) ) & ( for
f,
g being ( ( ) ( )
Morphism of ( ( ) ( )
set ) ) st
dom g : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) )
= cod f : ( ( ) ( )
Morphism of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) holds
it : ( (
Function-like quasi_total ) (
Relation-like D : ( ( ) ( )
set )
-defined C : ( (
V36() ) (
V36() )
set )
-valued Function-like quasi_total )
Element of
bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. (g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) (*) f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
C : ( (
V36() ) (
V36() )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
(*) (it : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( V36() ) ( V36() ) set ) -valued Function-like quasi_total ) Element of bool [:D : ( ( ) ( ) set ) ,C : ( ( V36() ) ( V36() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier' of
D : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) );
end;
theorem
for
C,
D being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
S being ( ( ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Contravariant_Functor of
C : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ,
D : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) )
for
c being ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) holds
S : ( ( ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Contravariant_Functor of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ,
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) )
. (id c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
= id ((Obj S : ( ( ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ,b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Morphism of
(Obj b3 : ( ( ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ,b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) ,
(Obj b3 : ( ( ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ,b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
C,
B,
D being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
S being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
C : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
for
T being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
D : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) holds
*' (T : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) * S : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
= T : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
* (*' S : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of (b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
C,
B,
D being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
S being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
C : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
for
T being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
D : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) holds
(T : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) * S : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
*' : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) )
= (T : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) *') : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) )
* S : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of (b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
C,
B,
D being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
F1 being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
C : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
for
F2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
B : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
D : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) holds
(*' (F2 : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) * F1 : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
b3 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
*' : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) )
= ((*' F2 : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -defined the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of (b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) *') : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) )
* ((*' F1 : ( ( Function-like quasi_total ) ( Relation-like the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of (b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -defined the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of the carrier' of (b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) ) *') : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of (b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of (b3 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
C,
D being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
S being ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
C : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
D : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) holds
(
*' S : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
= S : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
* (*id C : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) : ( ( ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Contravariant_Functor of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
opp : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) ,
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ) : ( (
Function-like ) (
Relation-like the
carrier' of
(b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of (b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) &
S : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) )
*' : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set ) )
= (id* D : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) : ( ( ) (
Relation-like the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Contravariant_Functor of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) ,
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
opp : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) )
* S : ( (
Function-like quasi_total ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) , the
carrier' of
b2 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set )
-defined the
carrier' of
(b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non
empty non
void strict ) ( non
empty non
void V55()
strict Category-like transitive associative reflexive with_identities )
CatStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier' of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier' of (b2 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) opp) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) ;
theorem
for
C being ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category)
for
a,
b,
c being ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) st
Hom (
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) &
Hom (
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool the
carrier' of
b1 : ( ( non
empty non
void Category-like transitive associative reflexive with_identities ) ( non
empty non
void V55()
Category-like transitive associative reflexive with_identities )
Category) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) )
<> {} : ( ( ) (
empty )
set ) holds
for
f being ( ( ) ( )
Morphism of
a : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) ( )
Morphism of
b : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) holds
g : ( ( ) ( )
Morphism of
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
* f : ( ( ) ( )
Morphism of
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Morphism of
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
= (f : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) )
* (g : ( ( ) ( ) Morphism of b3 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) opp) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Morphism of
b4 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) )
opp : ( ( ) ( )
Object of ( ( ) ( non
empty )
set ) ) ) ;