:: AUTALG_1 semantic presentation

begin

theorem :: AUTALG_1:1
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) holds id the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) : ( ( V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is_isomorphism UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ,UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;

definition
let UA be ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;
func UAAut UA -> ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) means :: AUTALG_1:def 1
 for h being ( ( Function-like quasi_total ) ( Relation-like the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( h : ( ( Function-like quasi_total ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) MSAlgebra over UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) iff h : ( ( Function-like quasi_total ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_isomorphism UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ,UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) );
end;

theorem :: AUTALG_1:2
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) holds UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) c= Funcs ( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:3
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) holds id the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) : ( ( V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:4
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for f, g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_isomorphism UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ,UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;

theorem :: AUTALG_1:5
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:6
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for f1, f2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) holds f1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) * f2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ;

definition
let UA be ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;
func UAAutComp UA -> ( ( Function-like quasi_total ) ( Relation-like [:(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ,(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14([:(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ,(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V118() ) BinOp of UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) means :: AUTALG_1:def 2
 for x, y being ( ( ) ( Relation-like the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) MSAlgebra over UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) . (x : ( ( ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like Function-like ) Element of UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) = y : ( ( ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) * x : ( ( ) ( Relation-like the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let UA be ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;
func UAAutGroup UA -> ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) equals :: AUTALG_1:def 3
 multMagma(# (UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ,(UAAutComp UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ,(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14([:(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ,(UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V118() ) BinOp of UAAut UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) , the carrier of UA : ( ( non empty ) ( non empty V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) #) : ( ( strict ) ( strict ) multMagma ) ;
end;

registration
let UA be ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ;
cluster UAAutGroup UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) UAStr ) : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) -> non empty strict Group-like associative ;
end;

theorem :: AUTALG_1:7
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f, g being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) * f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:8
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) holds id the carrier of UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) : ( ( V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = 1_ (UAAutGroup UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( ) Element of the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:9
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) = g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: AUTALG_1:10
for I being ( ( ) ( ) set )
for A, B, C being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) & B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to C : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: AUTALG_1:11
for x being ( ( ) ( ) set )
for A being ( ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like non empty V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ManySortedSet of {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) holds A : ( ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like non empty V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ManySortedSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) set ) .--> (A : ( ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like non empty V14({b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) ) ManySortedSet of {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined Function-like one-to-one ) set ) ;

theorem :: AUTALG_1:12
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
( F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" ) ;

theorem :: AUTALG_1:13
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
(F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "") : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: AUTALG_1:14
for F, G being ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V118() ) Function) st F : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V118() ) Function) is "1-1" & G : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V118() ) Function) is "1-1" holds
G : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V118() ) Function) ** F : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V118() ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V118() ) set ) is "1-1" ;

theorem :: AUTALG_1:15
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for B, C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" & G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" ;

theorem :: AUTALG_1:16
for I being ( ( ) ( ) set )
for A, B, C being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,C : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" & G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" holds
(G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = (F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "") : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** (G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "") : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b4 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: AUTALG_1:17
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of B : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "1-1" & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is "onto" & G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = id A : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) "" : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b3 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like V2() b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: AUTALG_1:18
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
(Funcs) (A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) set ) is V2() ;

definition
let I be ( ( ) ( ) set ) ;
let A, B be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
assume A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
func MSFuncs (A,B) -> ( ( non empty ) ( non empty ) set ) equals :: AUTALG_1:def 4
 product ((Funcs) (A : ( ( ) ( ) set ) ,B : ( ( ) ( Relation-like the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) ManySortedFunction of the Arity of I : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -valued Function-like quasi_total ) Element of bool [: the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * K266( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) ) : ( ( Relation-like K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) ( Relation-like K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) , the ResultSort of I : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of I : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * A : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ) )) : ( ( Relation-like I : ( ( non trivial ) ( non trivial ) set ) -defined Function-like V14(I : ( ( non trivial ) ( non trivial ) set ) ) ) ( Relation-like I : ( ( non trivial ) ( non trivial ) set ) -defined Function-like V14(I : ( ( non trivial ) ( non trivial ) set ) ) ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: AUTALG_1:19
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in MSFuncs (A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: AUTALG_1:20
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is_transformable_to B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
for g being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds g : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) in MSFuncs (A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like V14(b1 : ( ( ) ( ) set ) ) ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) set ) ;

registration
let I be ( ( ) ( ) set ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster (Funcs) (A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ,A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) -> Relation-like V2() I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let D be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let A be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: Element
redefine mode Element of A -> ( ( ) ( Relation-like I : ( ( non trivial ) ( non trivial ) set ) -defined Function-like V14(I : ( ( non trivial ) ( non trivial ) set ) ) Function-yielding V118() ) ManySortedFunction of D : ( ( ) ( ) set ) ,D : ( ( ) ( ) set ) ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster id A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ,A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ) -> "onto" ;
cluster id A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ,A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like V14(I : ( ( ) ( ) set ) ) ) set ) ) -> "1-1" ;
end;

begin

definition
let S be ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ;
let U1, U2 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ;
mode MSFunctionSet of U1,U2 is ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: AUTALG_1:21
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) holds id the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() "1-1" "onto" ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) in MSFuncs ( the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( non empty ) ( non empty ) set ) ;

definition
let S be ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ;
let U1 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ;
func MSAAut U1 -> ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) means :: AUTALG_1:def 5
 for h being ( ( ) ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of S : ( ( non trivial ) ( non trivial ) set ) ,S : ( ( non trivial ) ( non trivial ) set ) ) holds
( h : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) in it : ( ( ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) ManySortedFunction of the Arity of S : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * K266( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) : ( ( Relation-like K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) ( Relation-like K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) , the ResultSort of S : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * U1 : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ) iff h : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ,S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) is_isomorphism U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) );
end;

theorem :: AUTALG_1:22
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) )
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) holds f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) in MSFuncs ( the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( non empty ) ( non empty ) set ) ;

theorem :: AUTALG_1:23
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) holds MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) c= MSFuncs ( the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) : ( ( non empty ) ( non empty ) set ) ;

theorem :: AUTALG_1:24
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) holds id the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() "1-1" "onto" ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) in MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ;

theorem :: AUTALG_1:25
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) )
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) holds f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) "" : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) in MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ;

theorem :: AUTALG_1:26
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) )
for f1, f2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) holds f1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) ** f2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) in MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ;

theorem :: AUTALG_1:27
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for F being ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) )
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) st F : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) = 0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) .--> f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one Function-yielding V118() ) set ) holds
F : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) in MSAAut (MSAlg UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ,(MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ) ;

definition
let S be ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ;
let U1 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ;
func MSAAutComp U1 -> ( ( Function-like quasi_total ) ( Relation-like [:(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ,(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) :] : ( ( ) ( non empty ) set ) -defined MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) -valued Function-like non empty V14([:(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ,(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) :] : ( ( ) ( non empty ) set ) ) quasi_total ) BinOp of MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ) means :: AUTALG_1:def 6
 for x, y being ( ( ) ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) ManySortedFunction of the Arity of S : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * K266( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) : ( ( Relation-like K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) ( Relation-like K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) -defined Function-like V14(K263( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) M12( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) )) ) ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) , the ResultSort of S : ( ( non trivial ) ( non trivial ) set ) : ( ( Function-like quasi_total ) ( Relation-like the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier' of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) , the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * U1 : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ) . (x : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) ,y : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) ) : ( ( ) ( ) Element of MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ) = y : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) ** x : ( ( ) ( Relation-like the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) : ( ( ) ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) Function-yielding V118() ) ManySortedFunction of the Sorts of U1 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) set ) , the Sorts of U1 : ( ( ) ( ) set ) : ( ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) -defined Function-like V14( the carrier of S : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( ) set ) ) ) set ) ) ;
end;

definition
let S be ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ;
let U1 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ;
func MSAAutGroup U1 -> ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) equals :: AUTALG_1:def 7
 multMagma(# (MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ,(MSAAutComp U1 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ,(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) :] : ( ( ) ( non empty ) set ) -defined MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) -valued Function-like non empty V14([:(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ,(MSAAut U1 : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) :] : ( ( ) ( non empty ) set ) ) quasi_total ) BinOp of MSAAut U1 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) MSFunctionSet of U1 : ( ( ) ( ) set ) ,U1 : ( ( ) ( ) set ) ) ) #) : ( ( strict ) ( strict ) multMagma ) ;
end;

registration
let S be ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ;
let U1 be ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ;
cluster MSAAutGroup U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty Group-like associative ) Group) -> non empty strict Group-like associative ;
end;

theorem :: AUTALG_1:28
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f, g being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (MSAAutGroup b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) ** f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) ;

theorem :: AUTALG_1:29
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) holds id the Sorts of U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() "1-1" "onto" ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) = 1_ (MSAAutGroup U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( ) Element of the carrier of (MSAAutGroup b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:30
for S being ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign )
for U1 being ( ( non-empty ) ( non-empty ) MSAlgebra over S : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) )
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut U1 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) = g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) Element of MSAAut b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( non empty ) ( non empty ) MSFunctionSet of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ,b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) ) "" : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) Function-yielding V118() ) ManySortedFunction of the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) , the Sorts of b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) : ( ( Relation-like the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like non-empty non empty-yielding the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) -defined Function-like non empty V14( the carrier of b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) : ( ( ) ( non empty ) set ) ) ) set ) ) = g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of the carrier of (MSAAutGroup b2 : ( ( non-empty ) ( non-empty ) MSAlgebra over b1 : ( ( non empty non void ) ( non empty non void V59() ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: AUTALG_1:31
for UA1, UA2 being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) st UA1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ,UA2 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) are_similar holds
for F being ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign UA1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign UA1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) holds F : ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) . 0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: AUTALG_1:32
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for f being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) holds 0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) .--> f : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined UAAut b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) -valued Function-like one-to-one Function-yielding V118() ) set ) is ( ( ) ( Relation-like the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) -defined Function-like non empty V14( the carrier of (MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) : ( ( ) ( non empty trivial V31() ) set ) ) Function-yielding V118() ) ManySortedFunction of (MSSign UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ,(MSSign UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ;

theorem :: AUTALG_1:33
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) .--> x : ( ( ) ( ) set ) : ( ( ) ( Relation-like {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined Function-like one-to-one ) set ) ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ( ( Function-like quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of (MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of UAAutGroup UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ;

theorem :: AUTALG_1:34
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra)
for h being ( ( Function-like quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of (MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of UAAutGroup UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) st ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in UAAut UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( ) ( non empty ) set ) ) holds
h : ( ( Function-like quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of (MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) .--> x : ( ( ) ( ) set ) : ( ( ) ( Relation-like {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined {0 : ( ( ) ( Function-like functional empty V24() V25() V26() V28() V29() V30() ) Element of K119() : ( ( ) ( non empty V24() V25() V26() ) Element of bool K115() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) -defined Function-like one-to-one ) set ) ) holds
h : ( ( Function-like quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) ( Relation-like the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of (MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) quasi_total V104( UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) ) Homomorphism of UAAutGroup b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) ) is bijective ;

theorem :: AUTALG_1:35
for UA being ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) holds UAAutGroup UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) , MSAAutGroup (MSAlg UA : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) ) : ( ( strict ) ( strict non-empty ) MSAlgebra over MSSign b1 : ( ( non empty V144() quasi_total non-empty ) ( non empty V144() quasi_total non-empty ) Universal_Algebra) : ( ( trivial non void strict segmental ) ( non empty trivial V53() non void 1 : ( ( ) ( non empty ) set ) -element V59() strict segmental ) ManySortedSign ) ) : ( ( non empty Group-like associative ) ( non empty strict Group-like associative ) Group) are_isomorphic ;