begin
definition
let G be ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ;
func Aut G -> ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
means
( ( for
f being ( ( ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like V14( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
quasi_total )
Element of
it : ( (
Function-like quasi_total ) (
Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set )
-defined G : ( ( ) ( )
doubleLoopStr )
-valued Function-like quasi_total )
Element of
bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) holds
f : ( (
Function-like quasi_total V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) is ( (
Function-like quasi_total V102(
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
quasi_total unity-preserving V102(
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) )
Homomorphism of
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) ) & ( for
h being ( (
Function-like quasi_total V102(
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
quasi_total unity-preserving V102(
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) )
Homomorphism of
G : ( ( ) ( )
doubleLoopStr ) ,
G : ( ( ) ( )
doubleLoopStr ) ) holds
(
h : ( (
Function-like quasi_total V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) )
in it : ( (
Function-like quasi_total ) (
Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set )
-defined G : ( ( ) ( )
doubleLoopStr )
-valued Function-like quasi_total )
Element of
bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) iff (
h : ( (
Function-like quasi_total V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) is
one-to-one &
h : ( (
Function-like quasi_total V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) is
onto ) ) ) );
end;
theorem
for
G being ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group)
for
h being ( (
Function-like quasi_total V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) holds
(
h : ( (
Function-like quasi_total V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) )
in Aut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) iff
h : ( (
Function-like quasi_total V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total unity-preserving V102(
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) )
Homomorphism of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ,
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ) is
bijective ) ;
definition
let G be ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ;
func AutComp G -> ( (
Function-like quasi_total ) (
Relation-like [:(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) ,(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) :] : ( ( ) ( )
set )
-defined Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
-valued Function-like V14(
[:(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) ,(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) :] : ( ( ) ( )
set ) )
quasi_total )
BinOp of
Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) )
means
for
x,
y being ( ( ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like V14( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
quasi_total )
Element of
Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) ) holds
it : ( (
Function-like quasi_total ) (
Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set )
-defined G : ( ( ) ( )
doubleLoopStr )
-valued Function-like quasi_total )
Element of
bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
. (
x : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Aut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) ,
y : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Aut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like Function-like )
Element of
Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) )
= x : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Aut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) )
* y : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Aut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like )
Element of
bool [: the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
end;
definition
let G be ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ;
func AutGroup G -> ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group)
equals
multMagma(#
(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) ,
(AutComp G : ( ( ) ( ) doubleLoopStr ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) ,(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) :] : ( ( ) ( )
set )
-defined Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
-valued Function-like V14(
[:(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) ,(Aut G : ( ( ) ( ) doubleLoopStr ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) ) :] : ( ( ) ( )
set ) )
quasi_total )
BinOp of
Aut G : ( ( ) ( )
doubleLoopStr ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) ) #) : ( (
strict ) (
strict )
multMagma ) ;
end;
definition
let G be ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) ;
func InnAut G -> ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
means
for
f being ( ( ) (
Relation-like the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-defined the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set )
-valued Function-like V14( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
quasi_total )
Element of
Funcs ( the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) , the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) ) holds
(
f : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Funcs ( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) )
in it : ( (
Function-like quasi_total ) (
Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set )
-defined G : ( ( ) ( )
doubleLoopStr )
-valued Function-like quasi_total )
Element of
bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) iff ex
a being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st
for
x being ( ( ) ( )
Element of ( ( ) ( )
set ) ) holds
f : ( ( ) (
Relation-like the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
Funcs ( the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) )
. x : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) )
= x : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
|^ a : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
G : ( ( ) ( )
doubleLoopStr ) : ( ( ) ( )
set ) ) );
end;
theorem
for
G being ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group)
for
f,
g being ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
InnAut G : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) holds
(AutComp G : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Aut b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ,(Aut b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( )
set )
-defined Aut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
-valued Function-like V14(
[:(Aut b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) ,(Aut b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( )
set ) )
quasi_total )
BinOp of
Aut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) )
. (
f : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
InnAut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) ,
g : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
InnAut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
InnAut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) )
* g : ( ( ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
InnAut b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty V14( the
carrier of
b1 : ( ( non
empty strict Group-like associative ) ( non
empty strict unital Group-like associative )
Group) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict Group-like associative ) ( non empty strict unital Group-like associative ) Group) : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;