:: GRCAT_1 semantic presentation

begin

theorem :: GRCAT_1:1
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for u1, u2, u3, u4 being ( ( ) ( ) Element of UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) holds
( [u1 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ,u2 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ,u3 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ] : ( ( ) ( V27() V28() ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & [u1 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ,u2 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ,u3 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ,u4 : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ] : ( ( ) ( V27() V28() V29() ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ;

theorem :: GRCAT_1:2
( op2 : ( ( Function-like quasi_total ) ( Relation-like [:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ({} : ( ( ) ( empty ) set ) ,{} : ( ( ) ( empty ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) & op1 : ( ( Function-like quasi_total ) ( Relation-like 1 : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {} : ( ( ) ( empty ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) & op0 : ( ( ) ( empty ) Element of 1 : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty ) set ) ) ;

theorem :: GRCAT_1:3
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds
( {{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & [{{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) ,{{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) ] : ( ( ) ( V27() ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & [:{{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) ,{{} : ( ( ) ( empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & op2 : ( ( Function-like quasi_total ) ( Relation-like [:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & op1 : ( ( Function-like quasi_total ) ( Relation-like 1 : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) ;

registration
cluster Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) -> midpoint_operator ;
end;

theorem :: GRCAT_1:4
( ( for x being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) holds x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) = {} : ( ( ) ( empty ) set ) ) & ( for x, y being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) holds x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) + y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) ) = {} : ( ( ) ( empty ) set ) ) & ( for x being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) holds - x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of ( ( ) ( non empty trivial V34() ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) ) = {} : ( ( ) ( empty ) set ) ) & 0. Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( V50( Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) ) left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable ) Element of the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) ) = {} : ( ( ) ( empty ) set ) ) ;

definition
let C be ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ;
let O be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
func Morphs O -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: GRCAT_1:def 1
 union { (Hom (a : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of bool the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where a, b is ( ( ) ( ) Object of ( ( ) ( ) set ) ) : ( a : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) in O : ( ( ) ( ) set ) & b : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) in O : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
end;

registration
let C be ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ;
let O be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
cluster Morphs O : ( ( non empty ) ( non empty ) Element of bool the carrier of C : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;
end;

definition
let C be ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ;
let O be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
func dom O -> ( ( Function-like quasi_total ) ( Relation-like Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined O : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,O : ( ( ) ( ) set ) ) equals :: GRCAT_1:def 2
 the Source of C : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | (Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
func cod O -> ( ( Function-like quasi_total ) ( Relation-like Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined O : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,O : ( ( ) ( ) set ) ) equals :: GRCAT_1:def 3
 the Target of C : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | (Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
func comp O -> ( ( Function-like ) ( Relation-like [:(Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like ) PartFunc of ,) equals :: GRCAT_1:def 4
 the Comp of C : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like ) ( Relation-like [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:[: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) || (Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) ;
canceled;
end;

definition
let C be ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ;
let O be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
func cat O -> ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of C : ( ( non trivial ) ( non trivial ) set ) ) equals :: GRCAT_1:def 6
 CatStr(# O : ( ( ) ( ) set ) ,(Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(dom O : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined O : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,O : ( ( ) ( ) set ) ) ,(cod O : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined O : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,O : ( ( ) ( ) set ) ) ,(comp O : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like [:(Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,(Morphs O : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier' of C : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Morphs O : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued Function-like ) PartFunc of ,) #) : ( ( strict ) ( strict ) CatStr ) ;
end;

registration
let C be ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ;
let O be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
cluster cat O : ( ( non empty ) ( non empty ) Element of bool the carrier of C : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) CatStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of C : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) CatStr ) ) -> strict ;
end;

theorem :: GRCAT_1:5
for C being ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category)
for O being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) holds the carrier of (cat O : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) Subcategory of b1 : ( ( non empty non void Category-like transitive associative reflexive with_identities ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Category) ) : ( ( ) ( non empty ) set ) = O : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;

definition
let G be ( ( non empty ) ( non empty ) 1-sorted ) ;
let H be ( ( non empty ) ( non empty ) ZeroStr ) ;
func ZeroMap (G,H) -> ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) equals :: GRCAT_1:def 7
 the carrier of G : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) --> (0. H : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of H : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of G : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of H : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: GRCAT_1:6
comp Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) -defined the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) , the carrier of Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) : ( ( ) ( non empty trivial V34() ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = op1 : ( ( Function-like quasi_total ) ( Relation-like 1 : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
let G be ( ( non empty ) ( non empty ) addMagma ) ;
let H be ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ;
cluster ZeroMap (G : ( ( non empty ) ( non empty ) addMagma ) ,H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total additive ;
end;

registration
let G be ( ( non empty ) ( non empty ) addMagma ) ;
let H be ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ;
cluster Relation-like the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive for ( ( ) ( ) Element of bool [: the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) , the carrier of H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: GRCAT_1:7
for G1, G2, G3 being ( ( non empty ) ( non empty ) addMagma )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is additive ;

registration
let G1 be ( ( non empty ) ( non empty ) addMagma ) ;
let G2, G3 be ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ;
let f be ( ( Function-like quasi_total additive ) ( Relation-like the carrier of G1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
let g be ( ( Function-like quasi_total additive ) ( Relation-like the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of G3 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total additive ) ( Relation-like the carrier of G1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Element of bool [: the carrier of G1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * g : ( ( Function-like quasi_total additive ) ( Relation-like the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of G3 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Element of bool [: the carrier of G2 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of G3 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) -> Function-like quasi_total additive for ( ( Function-like quasi_total ) ( Relation-like the carrier of G1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of G3 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

definition
attr c1 is strict ;
struct GroupMorphismStr -> ;
aggr GroupMorphismStr(# Source, Target, Fun #) -> ( ( strict ) ( strict ) GroupMorphismStr ) ;
sel Source c1 -> ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
sel Target c1 -> ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
sel Fun c1 -> ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of c1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of c1 : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

definition
canceled;
let f be ( ( ) ( ) GroupMorphismStr ) ;
func dom f -> ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) equals :: GRCAT_1:def 9
 the Source of f : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
func cod f -> ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) equals :: GRCAT_1:def 10
 the Target of f : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
end;

definition
let f be ( ( ) ( ) GroupMorphismStr ) ;
func fun f -> ( ( Function-like quasi_total ) ( Relation-like the carrier of (dom f : ( ( non empty ) ( non empty ) addMagma ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of (cod f : ( ( non empty ) ( non empty ) addMagma ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) equals :: GRCAT_1:def 11
 the Fun of f : ( ( non empty ) ( non empty ) addMagma ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of f : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of f : ( ( non empty ) ( non empty ) addMagma ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

theorem :: GRCAT_1:8
for f being ( ( ) ( ) GroupMorphismStr )
for G1, G2 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for f0 being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( ) ( ) GroupMorphismStr ) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) holds
( dom f : ( ( ) ( ) GroupMorphismStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & cod f : ( ( ) ( ) GroupMorphismStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & fun f : ( ( ) ( ) GroupMorphismStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (dom b1 : ( ( ) ( ) GroupMorphismStr ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of (cod b1 : ( ( ) ( ) GroupMorphismStr ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
func ZERO (G,H) -> ( ( ) ( ) GroupMorphismStr ) equals :: GRCAT_1:def 12
 GroupMorphismStr(# G : ( ( non empty ) ( non empty ) addMagma ) ,H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ,(ZeroMap (G : ( ( non empty ) ( non empty ) addMagma ) ,H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ;
end;

registration
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
cluster ZERO (G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) GroupMorphismStr ) -> strict ;
end;

definition
let IT be ( ( ) ( ) GroupMorphismStr ) ;
attr IT is GroupMorphism-like means :: GRCAT_1:def 13
 fun IT : ( ( non empty ) ( non empty ) addMagma ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (dom IT : ( ( non empty ) ( non empty ) addMagma ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of (cod IT : ( ( non empty ) ( non empty ) addMagma ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive ;
end;

registration
cluster strict GroupMorphism-like for ( ( ) ( ) GroupMorphismStr ) ;
end;

definition
mode GroupMorphism is ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphismStr ) ;
end;

theorem :: GRCAT_1:9
for F being ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) holds the Fun of F : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of b1 : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of b1 : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive ;

registration
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
cluster ZERO (G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( strict ) GroupMorphismStr ) -> GroupMorphism-like ;
end;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
mode Morphism of G,H -> ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) means :: GRCAT_1:def 14
( dom it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty ) ( non empty ) addMagma ) & cod it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = H : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) );
end;

registration
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
cluster strict GroupMorphism-like for ( ( ) ( ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

theorem :: GRCAT_1:10
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for f being ( ( strict ) ( strict ) GroupMorphismStr ) st dom f : ( ( strict ) ( strict ) GroupMorphismStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & cod f : ( ( strict ) ( strict ) GroupMorphismStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & fun f : ( ( strict ) ( strict ) GroupMorphismStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (dom b3 : ( ( strict ) ( strict ) GroupMorphismStr ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of (cod b3 : ( ( strict ) ( strict ) GroupMorphismStr ) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive holds
f : ( ( strict ) ( strict ) GroupMorphismStr ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

theorem :: GRCAT_1:11
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive holds
GroupMorphismStr(# G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

registration
let G be ( ( non empty ) ( non empty ) addMagma ) ;
cluster id G : ( ( non empty ) ( non empty ) addMagma ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -defined the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addMagma ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> Function-like quasi_total additive ;
end;

definition
let G be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
func ID G -> ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) equals :: GRCAT_1:def 15
 GroupMorphismStr(# G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,(id G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total additive ) Element of bool [: the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ;
end;

registration
let G be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
cluster ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) -> strict ;
end;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
:: original: ZERO
redefine func ZERO (G,H) -> ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

theorem :: GRCAT_1:12
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for F being ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( GroupMorphismStr(# the Source of F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Target of F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Fun of F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of b3 : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of b3 : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) = GroupMorphismStr(# G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive ) ;

theorem :: GRCAT_1:13
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for F being ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st F : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) = GroupMorphismStr(# G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ;

theorem :: GRCAT_1:14
for F being ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) ex G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) st F : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) is ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

theorem :: GRCAT_1:15
for F being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ex G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( F : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) is ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) & F : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = GroupMorphismStr(# G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is additive ) ;

theorem :: GRCAT_1:16
for g, f being ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) st dom g : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod f : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
ex G1, G2, G3 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) st
( g : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) is ( ( ) ( GroupMorphism-like ) Morphism of G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) & f : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) is ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ) ;

definition
let G, F be ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) ;
assume dom G : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod F : ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
func G * F -> ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) means :: GRCAT_1:def 16
 for G1, G2, G3 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st GroupMorphismStr(# the Source of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Target of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Fun of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) = GroupMorphismStr(# G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & GroupMorphismStr(# the Source of F : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Target of F : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) , the Fun of F : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of the Source of F : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of the Target of F : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) holds
it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,(g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ;
end;

theorem :: GRCAT_1:17
for G1, G2, G3 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for G being ( ( ) ( GroupMorphism-like ) Morphism of G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) )
for F being ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) holds G : ( ( ) ( GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) is ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

definition
let G1, G2, G3 be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
let G be ( ( ) ( GroupMorphism-like ) Morphism of G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;
let F be ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;
:: original: *
redefine func G * F -> ( ( strict ) ( strict GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,G3 : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ) ;
end;

theorem :: GRCAT_1:18
for G1, G2, G3 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for G being ( ( ) ( GroupMorphism-like ) Morphism of G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) )
for F being ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st G : ( ( ) ( GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) = GroupMorphismStr(# G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) holds
G : ( ( ) ( GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * F : ( ( ) ( GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,(g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ;

theorem :: GRCAT_1:19
for f, g being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) st dom g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
ex G1, G2, G3 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ex f0 being ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ex g0 being ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,f0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = GroupMorphismStr(# G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,g0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) & g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = GroupMorphismStr(# G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,(g0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f0 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) GroupMorphismStr ) ) ;

theorem :: GRCAT_1:20
for f, g being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) st dom g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
( dom (g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = dom f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & cod (g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

theorem :: GRCAT_1:21
for G1, G2, G3, G4 being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for f being ( ( strict ) ( strict GroupMorphism-like ) Morphism of G1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) )
for g being ( ( strict ) ( strict GroupMorphism-like ) Morphism of G2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) )
for h being ( ( strict ) ( strict GroupMorphism-like ) Morphism of G3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,G4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) holds h : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * (g : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * f : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ) : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) = (h : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * g : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ) : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * f : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

theorem :: GRCAT_1:22
for f, g, h being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) st dom h : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & dom g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = cod f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
h : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * (g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = (h : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ;

theorem :: GRCAT_1:23
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
( dom (ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & cod (ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & ( for f being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) st cod f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
(ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) * f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) & ( for g being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) st dom g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) = G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) * (ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) = g : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) ) ;

definition
let IT be ( ( ) ( ) set ) ;
attr IT is Group_DOMAIN-like means :: GRCAT_1:def 17
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in IT : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) holds
x : ( ( ) ( ) set ) is ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
end;

registration
cluster non empty Group_DOMAIN-like for ( ( ) ( ) set ) ;
end;

definition
mode Group_DOMAIN is ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) set ) ;
end;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
:: original: Element
redefine mode Element of V -> ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
end;

registration
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for ( ( ) ( ) Element of V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) set ) ) ;
end;

definition
let IT be ( ( ) ( ) set ) ;
attr IT is GroupMorphism_DOMAIN-like means :: GRCAT_1:def 18
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in IT : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) set ) holds
x : ( ( ) ( ) set ) is ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ;
end;

registration
cluster non empty GroupMorphism_DOMAIN-like for ( ( ) ( ) set ) ;
end;

definition
mode GroupMorphism_DOMAIN is ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) ;
end;

definition
let M be ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ;
:: original: Element
redefine mode Element of M -> ( ( GroupMorphism-like ) ( GroupMorphism-like ) GroupMorphism) ;
end;

registration
let M be ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ;
cluster strict GroupMorphism-like for ( ( ) ( ) Element of M : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) ) ;
end;

theorem :: GRCAT_1:24
for f being ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) holds {f : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) } : ( ( ) ( non empty ) set ) is ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
mode GroupMorphism_DOMAIN of G,H -> ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) means :: GRCAT_1:def 19
 for x being ( ( ) ( GroupMorphism-like ) Element of it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) ) holds x : ( ( ) ( GroupMorphism-like ) Element of ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

theorem :: GRCAT_1:25
for D being ( ( non empty ) ( non empty ) set )
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) holds
( D : ( ( non empty ) ( non empty ) set ) is ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) iff for x being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ) ;

theorem :: GRCAT_1:26
for G, H being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup)
for f being ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) holds {f : ( ( strict ) ( strict GroupMorphism-like ) Morphism of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) } : ( ( ) ( non empty ) set ) is ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;

definition
let G, H be ( ( ) ( ) 1-sorted ) ;
mode MapsSet of G,H -> ( ( ) ( ) set ) means :: GRCAT_1:def 20
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) holds
x : ( ( ) ( ) set ) is ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

definition
let G, H be ( ( ) ( ) 1-sorted ) ;
func Maps (G,H) -> ( ( ) ( ) MapsSet of G : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) equals :: GRCAT_1:def 21
 Funcs ( the carrier of G : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) set ) : ( ( ) ( ) set ) , the carrier of H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) set ) ;
end;

registration
let G be ( ( ) ( ) 1-sorted ) ;
let H be ( ( non empty ) ( non empty ) 1-sorted ) ;
cluster Maps (G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) MapsSet of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty ;
end;

registration
let G be ( ( ) ( ) 1-sorted ) ;
let H be ( ( non empty ) ( non empty ) 1-sorted ) ;
cluster non empty for ( ( ) ( ) MapsSet of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
end;

definition
let G be ( ( ) ( ) 1-sorted ) ;
let H be ( ( non empty ) ( non empty ) 1-sorted ) ;
let M be ( ( non empty ) ( non empty ) MapsSet of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
:: original: Element
redefine mode Element of M -> ( ( Function-like quasi_total ) ( Relation-like the carrier of G : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of H : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
func Morphs (G,H) -> ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) means :: GRCAT_1:def 22
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( non empty right_zeroed ) ( non empty right_zeroed ) addLoopStr ) iff x : ( ( ) ( ) set ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) );
end;

definition
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
let M be ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;
:: original: Element
redefine mode Element of M -> ( ( ) ( GroupMorphism-like ) Morphism of G : ( ( ) ( ) 1-sorted ) ,H : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
end;

registration
let G, H be ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;
let M be ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) ;
cluster strict GroupMorphism-like for ( ( ) ( ) Element of M : ( ( ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,H : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ) ;
end;

definition
let x, y be ( ( ) ( ) set ) ;
pred GO x,y means :: GRCAT_1:def 23
 ex x1, x2, x3, x4 being ( ( ) ( ) set ) st
( x : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) = [x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ] : ( ( ) ( V27() V28() V29() ) set ) & ex G being ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) st
( y : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) = G : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) & x1 : ( ( ) ( ) set ) = the carrier of G : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) & x2 : ( ( ) ( ) set ) = the addF of G : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[: the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & x3 : ( ( ) ( ) set ) = comp G : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -defined the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) , the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & x4 : ( ( ) ( ) set ) = 0. G : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( V50(b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ) left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Element of the carrier of b5 : ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: GRCAT_1:27
for x, y1, y2 being ( ( ) ( ) set ) st GO x : ( ( ) ( ) set ) ,y1 : ( ( ) ( ) set ) & GO x : ( ( ) ( ) set ) ,y2 : ( ( ) ( ) set ) holds
y1 : ( ( ) ( ) set ) = y2 : ( ( ) ( ) set ) ;

theorem :: GRCAT_1:28
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ex x being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) & GO x : ( ( ) ( ) set ) , Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) ) ;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func GroupObjects UN -> ( ( ) ( ) set ) means :: GRCAT_1:def 24
 for y being ( ( ) ( ) set ) holds
( y : ( ( ) ( ) set ) in it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) iff ex x being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) & GO x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) );
end;

theorem :: GRCAT_1:29
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) in GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( ) set ) ;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: GRCAT_1:30
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for x being ( ( ) ( ) Element of GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty ) set ) ) is ( ( non empty strict right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AddGroup) ;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( non empty ) set ) -> Group_DOMAIN-like ;
end;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
func Morphs V -> ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) means :: GRCAT_1:def 25
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) iff ex G, H being ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) st x : ( ( ) ( ) set ) is ( ( strict ) ( strict GroupMorphism-like ) Morphism of G : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ,H : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ) );
end;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
let F be ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ;
:: original: dom
redefine func dom F -> ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
:: original: cod
redefine func cod F -> ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
let G be ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ;
func ID G -> ( ( strict ) ( strict GroupMorphism-like ) Element of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) equals :: GRCAT_1:def 26
 ID G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( strict GroupMorphism-like ) Morphism of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
func dom V -> ( ( Function-like quasi_total ) ( Relation-like Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -defined V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) -valued Function-like non empty total quasi_total ) Function of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) means :: GRCAT_1:def 27
 for f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) holds it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) . f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( ) ( ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) = dom f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
func cod V -> ( ( Function-like quasi_total ) ( Relation-like Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -defined V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) -valued Function-like non empty total quasi_total ) Function of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) means :: GRCAT_1:def 28
 for f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) holds it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) . f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( ) ( ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) = cod f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ;
end;

theorem :: GRCAT_1:31
for V being ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN)
for g, f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) st dom g : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) = cod f : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) holds
ex G1, G2, G3 being ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) st
( g : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) is ( ( ) ( GroupMorphism-like ) Morphism of G2 : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ,G3 : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ) & f : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) is ( ( ) ( GroupMorphism-like ) Morphism of G1 : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ,G2 : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) ) ) ;

theorem :: GRCAT_1:32
for V being ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN)
for g, f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) st dom g : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) = cod f : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ) holds
g : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) * f : ( ( ) ( GroupMorphism-like ) Element of Morphs b1 : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) in Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ;

definition
let V be ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) ;
func comp V -> ( ( Function-like ) ( Relation-like [:(Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,(Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) :] : ( ( ) ( non empty ) set ) -defined Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -valued Function-like ) PartFunc of ,) means :: GRCAT_1:def 29
( ( for g, f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) holds
( [g : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ,f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ] : ( ( ) ( V27() ) set ) in dom it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) iff dom g : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) = cod f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) ) ) & ( for g, f being ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) st [g : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ,f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ] : ( ( ) ( V27() ) set ) in dom it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) holds
it : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) . (g : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ,f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ) : ( ( ) ( ) set ) = g : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) * f : ( ( ) ( GroupMorphism-like ) Element of Morphs V : ( ( non empty Group_DOMAIN-like ) ( non empty Group_DOMAIN-like ) Group_DOMAIN) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) );
end;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func GroupCat UN -> ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) equals :: GRCAT_1:def 30
 CatStr(# (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ,(Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,(dom (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -defined GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) , GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) ) ,(cod (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -defined GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Function of Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) , GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( ) set ) ) ,(comp (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like [:(Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,(Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) :] : ( ( ) ( non empty ) set ) -defined Morphs (GroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -valued Function-like ) PartFunc of ,) #) : ( ( strict ) ( strict ) CatStr ) ;
end;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) -> non empty non void strict ;
end;

theorem :: GRCAT_1:33
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for f, g being ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) holds
( [g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ,f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V27() ) set ) in dom the Comp of (GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( Function-like ) ( Relation-like [: the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:[: the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) , the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) iff dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GRCAT_1:34
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for f being ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) )
for f9 being ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) )
for b being ( ( ) ( ) Object of ( ( ) ( non empty ) set ) )
for b9 being ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) holds
( f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) is ( ( strict ) ( strict GroupMorphism-like ) Element of Morphs (GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) & f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) is ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) is ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) & b9 : ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) is ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ;

theorem :: GRCAT_1:35
canceled;

theorem :: GRCAT_1:36
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for f, g being ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) )
for f9, g9 being ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) st f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) = f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) & g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) = g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) holds
( ( dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) implies dom g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = cod f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) ) & ( dom g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = cod f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) implies dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) ) & ( dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) implies [g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ,f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ] : ( ( ) ( V27() ) set ) in dom (comp (GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( Function-like ) ( Relation-like [:(Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,(Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) :] : ( ( ) ( non empty ) set ) -defined Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -valued Function-like ) PartFunc of ,) : ( ( ) ( Relation-like ) set ) ) & ( [g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ,f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ] : ( ( ) ( V27() ) set ) in dom (comp (GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( Function-like ) ( Relation-like [:(Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ,(Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) :] : ( ( ) ( non empty ) set ) -defined Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) -valued Function-like ) PartFunc of ,) : ( ( ) ( Relation-like ) set ) implies dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) ) & ( dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) implies g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) (*) f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier' of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) * f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict GroupMorphism-like ) ( strict GroupMorphism-like ) GroupMorphism) ) & ( dom f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) implies dom f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = dom g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) ) & ( dom f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = dom g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) implies dom f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = dom g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) ) & ( cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) implies cod f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = cod g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) ) & ( cod f9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) = cod g9 : ( ( ) ( GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) : ( ( strict ) ( non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) implies cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) = cod g : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) : ( ( ) ( non empty ) set ) ) ) ) ;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) -> non empty non void strict Category-like reflexive ;
end;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like reflexive ) CatStr ) -> non empty non void strict transitive associative with_identities ;
end;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func AbGroupObjects UN -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: GRCAT_1:def 31
 { G : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where G is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex H being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AbGroup) st G : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) AbGroup) } ;
end;

theorem :: GRCAT_1:37
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) in AbGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster AbGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;
end;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func AbGroupCat UN -> ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) ) equals :: GRCAT_1:def 32
 cat (AbGroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) ) ;
end;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster AbGroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) ) -> strict ;
end;

theorem :: GRCAT_1:38
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds the carrier of (AbGroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) ) : ( ( ) ( non empty ) set ) = AbGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func MidOpGroupObjects UN -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: GRCAT_1:def 33
 { G : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where G is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex H being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) AbGroup) st G : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) AbGroup) } ;
end;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster MidOpGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;
end;

definition
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
func MidOpGroupCat UN -> ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of AbGroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) ) ) equals :: GRCAT_1:def 34
 cat (MidOpGroupObjects UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of AbGroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) addLoopStr ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) ) ) ;
end;

registration
let UN be ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ;
cluster MidOpGroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( non empty non void V55() Category-like transitive associative reflexive with_identities ) Subcategory of AbGroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) ) ) -> strict ;
end;

theorem :: GRCAT_1:39
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds the carrier of (MidOpGroupCat UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) Subcategory of AbGroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) Subcategory of GroupCat b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( non empty non void strict ) ( non empty non void V55() strict Category-like transitive associative reflexive with_identities ) CatStr ) ) ) : ( ( ) ( non empty ) set ) = MidOpGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: GRCAT_1:40
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) holds Trivial-addLoopStr : ( ( ) ( non empty trivial V49() V54(1 : ( ( ) ( non empty ) set ) ) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator ) addLoopStr ) in MidOpGroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: GRCAT_1:41
for S, T being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = id T : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ") : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = id S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is onto ) ;

theorem :: GRCAT_1:42
for UN being ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe)
for a being ( ( ) ( ) Object of ( ( ) ( non empty ) set ) )
for aa being ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects UN : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) st a : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) = aa : ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) holds
id a : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Morphism of b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) = ID aa : ( ( ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ) Element of GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) : ( ( ) ( non empty Group_DOMAIN-like ) set ) ) : ( ( strict ) ( strict GroupMorphism-like ) Element of Morphs (GroupObjects b1 : ( ( non empty universal ) ( non empty V15() V22() V23() universal ) Universe) ) : ( ( ) ( non empty Group_DOMAIN-like ) set ) : ( ( non empty GroupMorphism_DOMAIN-like ) ( non empty GroupMorphism_DOMAIN-like ) GroupMorphism_DOMAIN) ) ;