let A be ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ;

let C1, C2 be ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ;
let F be ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ;
let A be ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of C1 : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ;

let X be ( ( ) ( ) set ) ;

for A being ( ( non empty ) ( non empty ) set )
for B, C being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) )
for D being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) st C : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) = D : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) holds
incl C : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b₃ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued b₃ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one non empty V14(b₃ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total onto ) Element of bool [:b₃ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) = (incl B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one non empty V14(b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total onto ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) * (incl D : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -valued b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one non empty V14(b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total onto ) Element of bool [:b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like one-to-one non empty V14(b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:b₄ : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

for X, Y being ( ( ) ( ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) ) is bijective holds
f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) ;

for X, Y being ( ( ) ( ) set )
for Z being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₂ : ( ( ) ( ) set ) ) quasi_total ) Function of Y : ( ( ) ( ) set ) ,Z : ( ( non empty ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) ) is bijective & g : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₂ : ( ( ) ( ) set ) ) quasi_total ) Function of b₂ : ( ( ) ( ) set ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) is bijective holds
ex h being ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₁ : ( ( ) ( ) set ) ) quasi_total ) Function of X : ( ( ) ( ) set ) ,Z : ( ( non empty ) ( non empty ) set ) ) st
( h : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₁ : ( ( ) ( ) set ) ) quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₂ : ( ( ) ( ) set ) ) quasi_total ) Function of b₂ : ( ( ) ( ) set ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₂ : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₂ : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like ) Element of bool [:b₁ : ( ( ) ( ) set ) ,b₃ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & h : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -valued Function-like V14(b₁ : ( ( ) ( ) set ) ) quasi_total ) Function of b₁ : ( ( ) ( ) set ) ,b₃ : ( ( non empty ) ( non empty ) set ) ) is bijective ) ;

for A being ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr )
for B being ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of A : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) )
for C being ( ( non empty ) ( non empty ) SubCatStr of A : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) )
for D being ( ( non empty ) ( non empty ) SubCatStr of B : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) st C : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) = D : ( ( non empty ) ( non empty ) SubCatStr of b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) holds
incl C : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) : ( ( strict ) ( reflexive feasible strict Covariant ) FunctorStr over b₃ : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ,b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) = (incl B : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) : ( ( strict ) ( reflexive feasible strict Covariant ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ,b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) * (incl D : ( ( non empty ) ( non empty ) SubCatStr of b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) ) : ( ( strict ) ( reflexive feasible strict Covariant ) FunctorStr over b₄ : ( ( non empty ) ( non empty ) SubCatStr of b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) : ( ( strict ) ( reflexive feasible strict Covariant ) FunctorStr over b₄ : ( ( non empty ) ( non empty ) SubCatStr of b₂ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) ,b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ;

for A, B being ( ( non empty ) ( non empty ) AltCatStr )
for F being ( ( ) ( ) FunctorStr over A : ( ( non empty ) ( non empty ) AltCatStr ) ,B : ( ( non empty ) ( non empty ) AltCatStr ) ) st F : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) is bijective holds
( the ObjectMap of F : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) is bijective & the MorphMap of F : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) : ( ( ) ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) V36() V37() ) MSUnTrans of the ObjectMap of b₃ : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Arrows of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( Relation-like [: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) ) is "1-1" ) ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is one-to-one & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is one-to-one holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is one-to-one ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is faithful & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is faithful holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is faithful ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is onto & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is onto holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is onto ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is full & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is full holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is full ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is injective & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is injective holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is injective ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is surjective & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is surjective holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is surjective ;

for C1 being ( ( non empty ) ( non empty ) AltGraph )
for C2, C3 being ( ( non empty reflexive ) ( non empty reflexive ) AltGraph )
for F being ( ( feasible ) ( feasible ) FunctorStr over C1 : ( ( non empty ) ( non empty ) AltGraph ) ,C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) )
for G being ( ( ) ( ) FunctorStr over C2 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,C3 : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is bijective & G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is bijective holds
G : ( ( ) ( ) FunctorStr over b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltGraph ) ,b₃ : ( ( non empty reflexive ) ( non empty reflexive ) AltGraph ) ) is bijective ;

for A, I being ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr )
for B being ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of A : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) )
for C being ( ( non empty ) ( non empty ) SubCatStr of A : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) )
for D being ( ( non empty ) ( non empty ) SubCatStr of B : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) st C : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) = D : ( ( non empty ) ( non empty ) SubCatStr of b₃ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) holds
for F being ( ( ) ( ) FunctorStr over A : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ,I : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) holds F : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) | C : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) : ( ( ) ( ) FunctorStr over b₄ : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) = (F : ( ( ) ( ) FunctorStr over b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) | B : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) : ( ( ) ( ) FunctorStr over b₃ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) | D : ( ( non empty ) ( non empty ) SubCatStr of b₃ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) : ( ( ) ( ) FunctorStr over b₅ : ( ( non empty ) ( non empty ) SubCatStr of b₃ : ( ( non empty reflexive ) ( non empty reflexive ) SubCatStr of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ) ,b₂ : ( ( non empty reflexive ) ( non empty reflexive ) AltCatStr ) ) ;

for A being ( ( non empty ) ( non empty ) AltCatStr )
for B being ( ( non empty ) ( non empty ) SubCatStr of A : ( ( non empty ) ( non empty ) AltCatStr ) ) holds
( B : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ) is full iff incl B : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ) : ( ( strict ) ( reflexive feasible strict Covariant ) FunctorStr over b₂ : ( ( non empty ) ( non empty ) SubCatStr of b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ) ,b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ) is full ) ;

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 ) ) holds
( F : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) is full iff for o1, o2 being ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) holds Morph-Map (F : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like <^b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) -defined <^(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ,(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:<^b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) ,<^(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ,(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is onto ) ;

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 ) ) holds
( F : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) is faithful iff for o1, o2 being ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) holds Morph-Map (F : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) ,o1 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,o2 : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like <^b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) -defined <^(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ,(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:<^b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ,b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) ,<^(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₄ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ,(b₃ : ( ( Covariant ) ( reflexive Covariant ) FunctorStr over b₁ : ( ( non empty ) ( non empty ) AltCatStr ) ,b₂ : ( ( non empty ) ( non empty ) AltCatStr ) ) . b₅ : ( ( ) ( ) object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty ) ( non empty ) AltCatStr ) : ( ( ) ( non empty ) set ) ) ^> : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is one-to-one ) ;

for A being ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) holds (id A : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( strict covariant ) ( reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective ) Functor of b₁ : ( ( 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 ) ) " : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( 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 ) ) = id A : ( ( non empty transitive with_units ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( strict covariant ) ( reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective ) Functor of b₁ : ( ( 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, B being ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr )
for F being ( ( feasible ) ( feasible ) FunctorStr over A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) is bijective holds
for G being ( ( feasible ) ( feasible ) FunctorStr over B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) st FunctorStr(# the ObjectMap of G : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the MorphMap of G : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) V36() V37() ) MSUnTrans of the ObjectMap of b₄ : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Arrows of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) " : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) holds
F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) * G : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( strict ) ( feasible strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = id B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( strict covariant ) ( reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective ) Functor of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ;

for A, B being ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr )
for F being ( ( feasible ) ( feasible ) FunctorStr over A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) is bijective holds
(F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ") : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) * F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = id A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( strict covariant ) ( reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective ) Functor of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ;

for A, B being ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr )
for F being ( ( feasible ) ( feasible ) FunctorStr over A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) is bijective holds
(F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ") : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) " : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = FunctorStr(# the ObjectMap of F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the MorphMap of F : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) V36() V37() ) MSUnTrans of the ObjectMap of b₃ : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Arrows of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ;

for A, B, C being ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr )
for G being ( ( feasible ) ( feasible ) FunctorStr over A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) )
for F being ( ( feasible ) ( feasible ) FunctorStr over B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,C : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) )
for GI being ( ( feasible ) ( feasible ) FunctorStr over B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,A : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) )
for FI being ( ( feasible ) ( feasible ) FunctorStr over C : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,B : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) st F : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) is bijective & G : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) is bijective & FunctorStr(# the ObjectMap of GI : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the MorphMap of GI : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) V36() V37() ) MSUnTrans of the ObjectMap of b₆ : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Arrows of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = G : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) " : ( ( strict ) ( strict ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) & FunctorStr(# the ObjectMap of FI : ( ( feasible ) ( feasible ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the MorphMap of FI : ( ( feasible ) ( feasible ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( ) ( Relation-like [: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) V36() V37() ) MSUnTrans of the ObjectMap of b₇ : ( ( feasible ) ( feasible ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -valued Function-like non empty V14([: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) quasi_total ) Element of bool [:[: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,[: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Arrows of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) , the Arrows of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) ( Relation-like [: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined Function-like non empty V14([: the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ) set ) ) #) : ( ( strict ) ( strict ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = F : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) " : ( ( strict ) ( strict ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) holds
(F : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) * G : ( ( feasible ) ( feasible ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ) : ( ( strict ) ( feasible strict ) FunctorStr over b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) " : ( ( strict ) ( strict ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) = GI : ( ( feasible ) ( feasible ) FunctorStr over b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) * FI : ( ( feasible ) ( feasible ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₂ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) : ( ( strict ) ( feasible strict ) FunctorStr over b₃ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ,b₁ : ( ( non empty transitive with_units reflexive ) ( non empty transitive with_units reflexive ) AltCatStr ) ) ;