attr R is multMagma-yielding means :: GROUP_7:def 1
for y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in rng R : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) holds
y : ( ( ) ( ) set ) is ( ( non empty ) ( non empty ) multMagma ) ;

cluster Relation-like Function-like multMagma-yielding -> Relation-like Function-like 1-sorted-yielding for ( ( ) ( ) set ) ;

cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding for ( ( ) ( ) set ) ;

cluster Relation-like Function-like multMagma-yielding for ( ( ) ( ) set ) ;

cluster Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) set ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) -> Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ;

func product F -> ( ( strict ) ( strict ) multMagma ) means :: GROUP_7:def 2
( the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = product (Carrier F : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) & ( for f, g being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( ) ( ) set ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) )
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex Fi being ( ( non empty ) ( non empty ) multMagma ) ex h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( Fi : ( ( non empty ) ( non empty ) multMagma ) = F : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) & h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = the multF of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (f : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) ,g : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) ) : ( ( ) ( ) set ) & h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) = the multF of Fi : ( ( non empty ) ( non empty ) multMagma ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) multMagma ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((f : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(g : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) );

cluster product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding ) set ) : ( ( strict ) ( strict ) multMagma ) -> non empty strict constituted-Functions ;

attr F is Group-like means :: GROUP_7:def 3
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex Fi being ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) st Fi : ( ( non empty commutative ) ( non empty commutative ) multMagma ) = F : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

attr F is associative means :: GROUP_7:def 4
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex Fi being ( ( non empty associative ) ( non empty associative ) multMagma ) st Fi : ( ( non empty commutative ) ( non empty commutative ) multMagma ) = F : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

attr F is commutative means :: GROUP_7:def 5
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) holds
ex Fi being ( ( non empty commutative ) ( non empty commutative ) multMagma ) st Fi : ( ( non empty commutative ) ( non empty commutative ) multMagma ) = F : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

redefine attr F is Group-like means :: GROUP_7:def 6
for i being ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) holds F : ( ( ) ( ) set ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) multMagma ) is Group-like ;

redefine attr F is associative means :: GROUP_7:def 7
for i being ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) holds F : ( ( ) ( ) set ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) multMagma ) is associative ;

redefine attr F is commutative means :: GROUP_7:def 8
for i being ( ( ) ( ) Element of I : ( ( ) ( ) set ) ) holds F : ( ( ) ( ) set ) . i : ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) multMagma ) is commutative ;

cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative commutative for ( ( ) ( ) set ) ;

cluster product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like ) set ) : ( ( strict ) ( non empty strict constituted-Functions ) multMagma ) -> strict Group-like ;

cluster product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding associative ) set ) : ( ( strict ) ( non empty strict constituted-Functions ) multMagma ) -> strict associative ;

cluster product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding commutative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding commutative ) set ) : ( ( strict ) ( non empty strict constituted-Functions ) multMagma ) -> strict commutative ;

func sum F -> ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( ) ( ) set ) : ( ( strict ) ( strict ) multMagma ) ) means :: GROUP_7:def 9
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined I : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:I : ( ( ) ( ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,I : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) iff ex g being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( ) ( ) set ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) ) ex J being ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) ex f being ( ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of J : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) ) st
( g : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) = 1_ (product F : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) multMagma ) : ( ( ) ( ) Element of the carrier of (product F : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) multMagma ) : ( ( ) ( ) set ) ) & x : ( ( ) ( ) set ) = g : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) multMagma-Family of I : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) -compatible total ) Element of product (Carrier F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) multMagma-Family of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional non empty with_common_domain product-like ) set ) ) +* f : ( ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & ( for j being ( ( ) ( ) set ) st j : ( ( ) ( ) set ) in J : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) holds
ex G being ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) st
( G : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) = F : ( ( ) ( ) set ) . j : ( ( ) ( ) set ) : ( ( ) ( ) set ) & f : ( ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) ) . j : ( ( ) ( ) set ) : ( ( ) ( ) set ) in the carrier of G : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) : ( ( ) ( non empty ) set ) & f : ( ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( Relation-like b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of b₃ : ( ( finite ) ( finite countable ) Subset of ( ( ) ( non empty ) set ) ) ) . j : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> 1_ G : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) : ( ( ) ( ) Element of the carrier of b₆ : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) : ( ( ) ( non empty ) set ) ) ) ) ) );

cluster the multF of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) , the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total associative ) Element of bool [:[: the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) , the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty ) set ) ) . (f : ( ( ) ( ) Element of the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) ) ,g : ( ( ) ( ) Element of the carrier of (sum F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) ) : ( ( strict ) ( non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) Subgroup of product F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total multMagma-yielding Group-like associative ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative ) set ) : ( ( strict ) ( non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() ) multMagma ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) -> Relation-like Function-like ;

cluster <*G1 : ( ( non empty ) ( non empty ) multMagma ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) -> {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined ;

cluster <*G1 : ( ( non empty ) ( non empty ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) -> total multMagma-yielding ;

cluster <*G1 : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable 1-sorted-yielding multMagma-yielding ) set ) -> Group-like ;

cluster <*G1 : ( ( non empty associative ) ( non empty associative ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable 1-sorted-yielding multMagma-yielding ) set ) -> associative ;

cluster <*G1 : ( ( non empty commutative ) ( non empty commutative ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable 1-sorted-yielding multMagma-yielding ) set ) -> commutative ;

cluster -> FinSequence-like for ( ( ) ( ) Element of product (Carrier <*G1 : ( ( ) ( ) set ) *> : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) ) : ( ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined Function-like total ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) ) ;

cluster -> FinSequence-like for ( ( ) ( ) Element of the carrier of (product <*G1 : ( ( ) ( ) set ) *> : ( ( Relation-like Function-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) ) : ( ( strict ) ( strict ) multMagma ) : ( ( ) ( ) set ) ) ;

cluster <*G1 : ( ( non empty ) ( non empty ) multMagma ) ,G2 : ( ( non empty ) ( non empty ) multMagma ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) -> {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined ;

cluster <*G1 : ( ( non empty ) ( non empty ) multMagma ) ,G2 : ( ( non empty ) ( non empty ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty finite V43(2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) set ) -> total multMagma-yielding ;

cluster <*G1 : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) ,G2 : ( ( non empty Group-like ) ( non empty unital Group-like ) multMagma ) *> : ( ( ) ( Relation-like {1 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty finite countable ) set ) -defined NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like non empty total finite V43(2 : ( ( ) ( non empty ext-real V27() V28() V29() V33() V34() V103() ) Element of NAT : ( ( ) ( non empty non trivial V27() V28() V29() non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable 1-sorted-yielding multMagma-yielding ) set ) -> Group-like ;