begin
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
o1,
o2,
o3 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
v being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
u being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
f being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
u : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* v : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) &
(f : ( ( ) ( ) Morphism of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) ") : ( ( ) ( )
M2(
<^b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) ))
* f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) ))
= idm o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2(
<^b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) )) &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
v : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= (f : ( ( ) ( ) Morphism of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) ") : ( ( ) ( )
M2(
<^b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) ))
* u : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
o2,
o3,
o1 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
v being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
u being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
f being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
u : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= v : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) &
f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* (f : ( ( ) ( ) Morphism of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) ") : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) ))
= idm o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) )) &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
v : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= u : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* (f : ( ( ) ( ) Morphism of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) ") : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set ) )) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
g,
h being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
h : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) ))
= idm o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) (
retraction coretraction iso mono epi )
M2(
<^b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) )) &
f : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
* g : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) ))
= idm o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) (
retraction coretraction iso mono epi )
M2(
<^b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) )) &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
g : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= h : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) ;
begin
begin
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
a being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) holds
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. (idm a : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
retraction coretraction mono epi )
M2(
<^b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( non
empty )
set ) )) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( non
empty )
set ) ))
= idm (F : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . a : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) )) : ( ( ) (
retraction coretraction mono epi )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( non
empty )
set ) )) ;
theorem
for
C1,
C2 being ( ( non
empty ) ( non
empty )
AltCatStr )
for
F being ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) holds
(
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
full iff for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) holds
Morph-Map (
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like <^b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
-defined <^(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set )
-valued Function-like quasi_total )
M2(
bool [:<^b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) ,<^(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) )) is
onto ) ;
theorem
for
C1,
C2 being ( ( non
empty ) ( non
empty )
AltCatStr )
for
F being ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) holds
(
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
faithful iff for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) holds
Morph-Map (
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like <^b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
-defined <^(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set )
-valued Function-like quasi_total )
M2(
bool [:<^b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) ,<^(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) )) is
one-to-one ) ;
theorem
for
C1,
C2 being ( ( non
empty ) ( non
empty )
AltCatStr )
for
F being ( (
Covariant ) (
reflexive Covariant )
FunctorStr over
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
Fm being ( ( ) ( )
Morphism of
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
(F : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) : ( ( ) ( non
empty )
set ) )) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
Covariant ) (
reflexive Covariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
full &
F : ( (
Covariant ) (
reflexive Covariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
feasible holds
ex
m being ( ( ) ( )
Morphism of
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
Fm : ( ( ) ( )
Morphism of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
(b3 : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) : ( ( ) ( non
empty )
set ) )) )
= F : ( (
Covariant ) (
reflexive Covariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) )
. m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) ;
theorem
for
C1,
C2 being ( ( non
empty ) ( non
empty )
AltCatStr )
for
F being ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
Fm being ( ( ) ( )
Morphism of
C2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
(F : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) : ( ( ) ( non
empty )
set ) )) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
full &
F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ) is
feasible holds
ex
m being ( ( ) ( )
Morphism of
C1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
Fm : ( ( ) ( )
Morphism of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) : ( ( ) ( non
empty )
set ) )) )
= F : ( (
Contravariant ) (
reflexive Contravariant )
FunctorStr over
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b2 : ( ( non
empty ) ( non
empty )
AltCatStr ) )
. m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty ) ( non
empty )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( Contravariant ) ( reflexive Contravariant ) FunctorStr over b1 : ( ( non empty ) ( non empty ) AltCatStr ) ,b2 : ( ( non empty ) ( non empty ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction holds
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
retraction ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction holds
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
coretraction ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso holds
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
iso ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction holds
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
coretraction ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction holds
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
retraction ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso holds
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
iso ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
full &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
retraction holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
full &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
coretraction holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
full &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( covariant ) ( reflexive feasible Covariant id-preserving comp-preserving covariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
iso holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) st
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
full &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) )) ,
F : ( (
covariant ) (
reflexive feasible Covariant id-preserving comp-preserving covariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) ))
are_iso holds
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
are_iso ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
full &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
retraction holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction ;
theorem
for
A,
B being ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr )
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
B : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
full &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b2 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
coretraction holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive with_units ) ( non
empty transitive with_units reflexive )
AltCatStr ) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
a being ( ( ) ( )
Morphism of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
full &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
M2(
<^(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b5 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ,(b3 : ( ( contravariant ) ( reflexive feasible Contravariant id-preserving comp-reversing contravariant ) Functor of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ,b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) ) . b4 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b2 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) )) ^> : ( ( ) ( )
set ) )) is
iso holds
a : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso ;
theorem
for
A,
B being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
F being ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
A : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
B : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) st
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
full &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) is
faithful &
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) )) ,
F : ( (
contravariant ) (
reflexive feasible Contravariant id-preserving comp-reversing contravariant )
Functor of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
. o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
M2( the
carrier of
b2 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) ))
are_iso holds
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
are_iso ;
begin
theorem
for
C being ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr )
for
D being ( ( non
empty transitive ) ( non
empty transitive )
SubCatStr of
C : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
n being ( ( ) ( )
Morphism of
D : ( ( non
empty transitive ) ( non
empty transitive )
SubCatStr of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ) ,
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive ) ( non
empty transitive )
SubCatStr of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) &
<^p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
( (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
mono implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive ) ( non
empty transitive )
SubCatStr of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
mono ) & (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
epi implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive ) ( non
empty transitive )
SubCatStr of
b1 : ( ( non
empty transitive ) ( non
empty transitive )
AltCatStr ) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
epi ) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
D being ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
m1 being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
n being ( ( ) ( )
Morphism of
D : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
n1 being ( ( ) ( )
Morphism of
D : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
p2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) &
m1 : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= n1 : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b6 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) &
<^p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
( (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_left_inverse_of m1 : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_left_inverse_of n1 : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b6 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) ) & (
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_left_inverse_of n1 : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b6 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) implies
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_left_inverse_of m1 : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) ) & (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_right_inverse_of m1 : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_right_inverse_of n1 : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b6 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) ) & (
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_right_inverse_of n1 : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b6 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) implies
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
is_right_inverse_of m1 : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b4 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
D being ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
n being ( ( ) ( )
Morphism of
D : ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) &
<^p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
( (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction ) & (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction ) & (
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso implies
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive full id-inheriting ) ( non
empty transitive V129()
with_units reflexive full id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso ) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category)
for
D being ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) )
for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
for
n being ( ( ) ( )
Morphism of
D : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) st
p1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
= o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) &
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
= n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) &
<^p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^p2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) holds
( (
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction implies
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction ) & (
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction implies
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction ) & (
n : ( ( ) ( )
Morphism of
b2 : ( ( non
empty transitive id-inheriting ) ( non
empty transitive V129()
with_units reflexive id-inheriting )
subcategory of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ,
b5 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso implies
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b3 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso ) ) ;
definition
let C be ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ;
func AllMono C -> ( ( non
empty transitive strict ) ( non
empty transitive strict V129() )
SubCatStr of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) )
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
= the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) & the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
cc= the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) & ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
in the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
. (
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
set ) iff (
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
mono ) ) ) );
end;
definition
let C be ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ;
func AllEpi C -> ( ( non
empty transitive strict ) ( non
empty transitive strict V129() )
SubCatStr of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) )
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
= the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) & the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
cc= the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) & ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
in the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
. (
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
set ) iff (
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
epi ) ) ) );
end;
definition
let C be ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ;
func AllRetr C -> ( ( non
empty transitive strict ) ( non
empty transitive strict V129() )
SubCatStr of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) )
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
= the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) & the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
cc= the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) & ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
in the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
. (
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
set ) iff (
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction ) ) ) );
end;
definition
let C be ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ;
func AllCoretr C -> ( ( non
empty transitive strict ) ( non
empty transitive strict V129() )
SubCatStr of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) )
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
= the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) & the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
cc= the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) & ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
in the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
. (
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
set ) iff (
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction ) ) ) );
end;
definition
let C be ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ;
func AllIso C -> ( ( non
empty transitive strict ) ( non
empty transitive strict V129() )
SubCatStr of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) )
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
= the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( ( ) ( non
empty )
set ) & the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
cc= the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) : ( (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of C : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) & ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
AltCatStr ) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) )
in the
Arrows of
it : ( ( ) ( )
set ) : ( (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined Function-like V14(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ) )
set )
. (
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ,
o2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
set ) iff (
<^o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) &
m : ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso ) ) ) );
end;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) st ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
mono ) holds
AltCatStr(# the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) , the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) , the
Comp of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V36()
V37() )
ManySortedFunction of
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ,
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ) #) : ( (
strict ) ( non
empty strict )
AltCatStr )
= AllMono C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( non
empty transitive strict ) ( non
empty transitive strict V129()
with_units reflexive id-inheriting )
SubCatStr of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) st ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
epi ) holds
AltCatStr(# the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) , the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) , the
Comp of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V36()
V37() )
ManySortedFunction of
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ,
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ) #) : ( (
strict ) ( non
empty strict )
AltCatStr )
= AllEpi C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( non
empty transitive strict ) ( non
empty transitive strict V129()
with_units reflexive id-inheriting )
SubCatStr of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) st ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
retraction &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) ) ) holds
AltCatStr(# the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) , the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) , the
Comp of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V36()
V37() )
ManySortedFunction of
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ,
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ) #) : ( (
strict ) ( non
empty strict )
AltCatStr )
= AllRetr C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( non
empty transitive strict ) ( non
empty transitive strict V129()
with_units reflexive id-inheriting )
SubCatStr of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) st ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
coretraction &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) ) ) holds
AltCatStr(# the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) , the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) , the
Comp of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V36()
V37() )
ManySortedFunction of
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ,
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ) #) : ( (
strict ) ( non
empty strict )
AltCatStr )
= AllCoretr C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( non
empty transitive strict ) ( non
empty transitive strict V129()
with_units reflexive id-inheriting )
SubCatStr of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ;
theorem
for
C being ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) st ( for
o1,
o2 being ( ( ) ( )
object of ( ( ) ( non
empty )
set ) )
for
m being ( ( ) ( )
Morphism of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
o1 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) holds
(
m : ( ( ) ( )
Morphism of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ,
b2 : ( ( ) ( )
object of ( ( ) ( non
empty )
set ) ) ) is
iso &
<^o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) ) ) holds
AltCatStr(# the
carrier of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) ( non
empty )
set ) , the
Arrows of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ) )
set ) , the
Comp of
C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V36()
V37() )
ManySortedFunction of
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ,
{| the Arrows of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) |} : ( (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined Function-like non
empty V14(
[: the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty transitive V129() with_units ) ( non empty transitive V129() with_units reflexive ) category) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) )
set ) ) #) : ( (
strict ) ( non
empty strict )
AltCatStr )
= AllIso C : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) : ( ( non
empty transitive strict ) ( non
empty transitive strict V129()
with_units reflexive id-inheriting )
SubCatStr of
b1 : ( ( non
empty transitive V129()
with_units ) ( non
empty transitive V129()
with_units reflexive )
category) ) ;