begin
definition
let R be ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ;
func TrivialLMod R -> ( ( non
empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( ) ( )
GroupMorphismStr ) )
equals
VectSpStr(# 1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
op2 : ( (
V6()
quasi_total ) (
V1()
V4(
[:1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( non
empty )
set ) )
V5(1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V6() non
empty V14(
[:1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[:1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
op0 : ( ( ) (
empty )
Element of 1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) ) ,
(pr2 ( the carrier of R : ( ( ) ( ) GroupMorphismStr ) : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( (
V6()
quasi_total ) (
V1()
V4(
[: the carrier of R : ( ( ) ( ) GroupMorphismStr ) : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( )
set ) )
V5(1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V6()
V14(
[: the carrier of R : ( ( ) ( ) GroupMorphismStr ) : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( )
set ) )
quasi_total )
Element of
bool [:[: the carrier of R : ( ( ) ( ) GroupMorphismStr ) : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
VectSpStr over
R : ( ( ) ( )
GroupMorphismStr ) ) ;
end;
definition
let R be ( ( non
empty ) ( non
empty )
multMagma ) ;
let G,
H be ( ( non
empty ) ( non
empty )
VectSpStr over
R : ( ( non
empty ) ( non
empty )
multMagma ) ) ;
let f be ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
G : ( ( non
empty ) ( non
empty )
VectSpStr over
R : ( ( non
empty ) ( non
empty )
multMagma ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
H : ( ( non
empty ) ( non
empty )
VectSpStr over
R : ( ( non
empty ) ( non
empty )
multMagma ) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
G : ( ( non
empty ) ( non
empty )
VectSpStr over
R : ( ( non
empty ) ( non
empty )
multMagma ) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) ;
attr f is
homogeneous means
for
a being ( ( ) ( )
Scalar of ( ( ) ( )
set ) )
for
x being ( ( ) ( )
Vector of ( ( ) ( )
set ) ) holds
f : ( (
V6()
quasi_total ) (
V1()
V4(
[:H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( )
set ) )
V5(
H : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
GroupMorphismStr ) ,
G : ( ( ) ( )
1-sorted ) ) )
V6()
quasi_total )
Element of
bool [:[:H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
. (a : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
G : ( ( ) ( )
1-sorted ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
H : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
GroupMorphismStr ) ,
G : ( ( ) ( )
1-sorted ) ) : ( ( ) ( )
set ) )
= a : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
* (f : ( ( V6() quasi_total ) ( V1() V4([:H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ) V5(H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) ) V6() quasi_total ) Element of bool [:[:H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,H : ( ( ) ( ) BiModStr over R : ( ( ) ( ) GroupMorphismStr ) ,G : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
H : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
GroupMorphismStr ) ,
G : ( ( ) ( )
1-sorted ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
H : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
GroupMorphismStr ) ,
G : ( ( ) ( )
1-sorted ) ) : ( ( ) ( )
set ) ) ;
end;
definition
let R be ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ;
let G,
H be ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ;
mode Morphism of
G,
H -> ( (
LModMorphism-like ) (
LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
means
(
dom it : ( (
V6()
quasi_total ) (
V1()
V4(
[:H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( )
set ) )
V5(
H : ( ( ) ( )
GroupMorphism_DOMAIN of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ,
G : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162()
V163()
V164()
V165() )
addLoopStr ) ) )
V6()
quasi_total )
Element of
bool [:[:H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( ) set ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
= G : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162()
V163()
V164()
V165() )
addLoopStr ) &
cod it : ( (
V6()
quasi_total ) (
V1()
V4(
[:H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( )
set ) )
V5(
H : ( ( ) ( )
GroupMorphism_DOMAIN of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ,
G : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162()
V163()
V164()
V165() )
addLoopStr ) ) )
V6()
quasi_total )
Element of
bool [:[:H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( ) set ) ,H : ( ( ) ( ) GroupMorphism_DOMAIN of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162() V163() V164() V165() ) addLoopStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
= H : ( ( ) ( )
GroupMorphism_DOMAIN of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ,
G : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed V162()
V163()
V164()
V165() )
addLoopStr ) ) );
end;
theorem
for
R being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring)
for
G,
H being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
for
F being ( ( ) (
LModMorphism-like )
Morphism of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
H : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) ex
f being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
(
LModMorphismStr(# the
Dom of
F : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) , the
Cod of
F : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) , the
Fun of
F : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of the
Dom of
b4 : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of the
Cod of
b4 : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of the
Dom of
b4 : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= LModMorphismStr(#
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
H : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
f : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) &
f : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
additive &
f : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
homogeneous ) ;
definition
let R be ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ;
let G,
F be ( (
LModMorphism-like ) (
LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ;
assume
dom G : ( (
LModMorphism-like ) (
LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= cod F : ( (
LModMorphism-like ) (
LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
;
func G * F -> ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
means
for
G1,
G2,
G3 being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
for
g being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
f being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
LModMorphismStr(# the
Dom of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) , the
Cod of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) , the
Fun of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of the
Dom of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of the
Cod of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of the
Dom of
G : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
= LModMorphismStr(#
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
g : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) &
LModMorphismStr(# the
Dom of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) , the
Cod of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) , the
Fun of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of the
Dom of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of the
Cod of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of the
Dom of
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
f : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) holds
it : ( (
V6()
quasi_total ) (
V1()
V4(
[:F : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ) ,F : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ) :] : ( ( ) ( )
set ) )
V5(
F : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
VectSpStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) )
V6()
quasi_total )
Element of
bool [:[:F : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ) ,F : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ) :] : ( ( ) ( ) set ) ,F : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) doubleLoopStr ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
(g : ( ( V6() quasi_total ) ( V1() V4( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( V6() quasi_total ) ( V1() V4( the carrier of b1 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b1 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( (
V6() ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b1 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) ) ;
end;
theorem
for
R being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring)
for
G2,
G3,
G1 being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
for
G being ( ( ) (
LModMorphism-like )
Morphism of
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
for
F being ( ( ) (
LModMorphism-like )
Morphism of
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
for
g being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
f being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
G : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
= LModMorphismStr(#
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
g : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) &
F : ( ( ) (
LModMorphism-like )
Morphism of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
f : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) holds
(
G : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
*' F : ( ( ) (
LModMorphism-like )
Morphism of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( (
strict ) (
strict LModMorphism-like )
Morphism of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
(g : ( ( V6() quasi_total ) ( V1() V4( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( V6() quasi_total ) ( V1() V4( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( (
V6() ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) &
G : ( ( ) (
LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
* F : ( ( ) (
LModMorphism-like )
Morphism of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
(g : ( ( V6() quasi_total ) ( V1() V4( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( V6() quasi_total ) ( V1() V4( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( (
V6() ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) ;
theorem
for
R being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring)
for
f,
g being ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) st
dom g : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= cod f : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) holds
ex
G1,
G2,
G3 being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ex
f0 being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) ex
g0 being ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b6 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
(
f : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
f0 : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) &
g : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= LModMorphismStr(#
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
g0 : ( (
V6()
quasi_total ) (
V1()
V4( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b6 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) &
g : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
* f : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= LModMorphismStr(#
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
(g0 : ( ( V6() quasi_total ) ( V1() V4( the carrier of b5 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b5 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f0 : ( ( V6() quasi_total ) ( V1() V4( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of b5 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) V6() non empty V14( the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( (
V6() ) (
V1()
V4( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b6 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14( the
carrier of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) , the carrier of b6 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
LModMorphismStr over
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) ;
theorem
for
R being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring)
for
G1,
G2,
G3,
G4 being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
R : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
for
f being ( (
strict ) (
strict LModMorphism-like )
Morphism of
G1 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
for
g being ( (
strict ) (
strict LModMorphism-like )
Morphism of
G2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
for
h being ( (
strict ) (
strict LModMorphism-like )
Morphism of
G3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
G4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) holds
h : ( (
strict ) (
strict LModMorphism-like )
Morphism of
b4 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b5 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) )
* (g : ( ( strict ) ( strict LModMorphism-like ) Morphism of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ,b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ) * f : ( ( strict ) ( strict LModMorphism-like ) Morphism of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ,b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
= (h : ( ( strict ) ( strict LModMorphism-like ) Morphism of b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ,b5 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ) * g : ( ( strict ) ( strict LModMorphism-like ) Morphism of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ,b4 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162() V163() V164() V165() ) Ring) ) ) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) )
* f : ( (
strict ) (
strict LModMorphism-like )
Morphism of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ,
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ) : ( (
strict LModMorphism-like ) (
strict LModMorphism-like )
LModMorphism of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
Ring) ) ;
definition
func add3 -> ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
means
for
a,
b being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) holds
it : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr )
. (
a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ;
func mult3 -> ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
means
for
a,
b being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) holds
it : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr )
. (
a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ;
func compl3 -> ( (
V6()
quasi_total ) (
V1()
V4(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
quasi_total )
UnOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
means
for
a being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) holds
it : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable V89()
associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr )
. a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= - a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ;
end;
definition
func Z_3 -> ( (
strict ) (
strict )
doubleLoopStr )
equals
doubleLoopStr(#
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ,
add3 : ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ,
mult3 : ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ,
unit3 : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ,
zero3 : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ;
end;
theorem
(
0. Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) (
V46(
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) ) )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= 0 : ( ( ) (
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
1. Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
0. Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) (
V46(
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) ) )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) is ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
1. Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) is ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) & the
addF of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( (
V6()
quasi_total ) (
V1()
V4(
[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= add3 : ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) & the
multF of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( (
V6()
quasi_total ) (
V1()
V4(
[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
Z_3 : ( (
strict ) ( non
empty strict V89()
right_unital well-unital left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of Z_3 : ( ( strict ) ( non empty strict V89() right_unital well-unital left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= mult3 : ( (
V6()
quasi_total ) (
V1()
V4(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
V5(
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
V6() non
empty V14(
[:{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
BinOp of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
x,
y being ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
for
X,
Y being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) st
X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) &
Y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= y : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) holds
(
x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
+ y : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ Y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
* y : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* Y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
- x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= - X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
x,
y,
z being ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
for
X,
Y,
Z being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) st
X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) &
Y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= y : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) &
Z : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= z : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) holds
(
(x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
+ z : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= (X : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) + Y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ Z : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
+ (y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + z : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ (Y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) + Z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
(x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
* z : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= (X : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * Y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* Z : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
* (y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * z : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
left_add-cancelable right_add-cancelable add-cancelable right_complementable )
Element of the
carrier of
Z_3 : ( (
strict ) ( non
empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict V89()
right_unital well-unital left_unital add-associative right_zeroed V162()
V163()
V164()
V165() )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= X : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* (Y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * Z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
x,
y,
z,
a,
b being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) st
a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= 0 : ( ( ) (
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) &
b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty )
Element of
K100() : ( ( ) ( )
Element of
bool K96() : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
(
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
(x : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ z : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ (y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) + z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ (- x : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
(x : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* z : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* (y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) & (
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
<> a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) implies ex
y being ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* y : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) &
a : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
<> b : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
* (y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) + z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
= (x : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) )
+ (x : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) * z : ( ( ) ( ) Element of {0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
{0 : ( ( ) ( empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty ) Element of K100() : ( ( ) ( ) Element of bool K96() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non
empty )
set ) ) ) ;