begin
definition
let A,
B,
C be ( ( non
empty ) ( non
empty )
set ) ;
let f be ( (
Function-like quasi_total ) ( non
empty Relation-like [:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined C : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V17(
[:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
C : ( ( non
empty ) ( non
empty )
set ) ) ;
~redefine func ~ f -> ( (
Function-like quasi_total ) ( non
empty Relation-like [:B : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined C : ( ( ) ( )
M29(
A : ( ( ) ( )
set ) ,
B : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like V17(
[:B : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[:B : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) ,
C : ( ( ) ( )
M29(
A : ( ( ) ( )
set ) ,
B : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) ;
end;
theorem
for
C,
A,
B being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like quasi_total ) ( non
empty Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V17(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
C : ( ( non
empty ) ( non
empty )
set ) )
for
x being ( ( ) ( )
Element of
A : ( ( non
empty ) ( non
empty )
set ) )
for
y being ( ( ) ( )
Element of
B : ( ( non
empty ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V17(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) )
. (
x : ( ( ) ( )
Element of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
y : ( ( ) ( )
Element of
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= (~ f : ( ( Function-like quasi_total ) ( non empty Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V17([:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) quasi_total ) Function of [:b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V17(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[:b3 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b1 : ( ( non
empty ) ( non
empty )
set ) )
. (
y : ( ( ) ( )
Element of
b3 : ( ( non
empty ) ( non
empty )
set ) ) ,
x : ( ( ) ( )
Element of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ;
begin
definition
let K be ( ( non
empty ) ( non
empty )
doubleLoopStr ) ;
func opp K -> ( (
strict ) (
strict )
doubleLoopStr )
equals
doubleLoopStr(# the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set ) , the
addF of
K : ( ( ) ( )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ,
(~ the multF of K : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like V17(
[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
(1. K : ( ( ) ( ) set ) ) : ( ( ) ( )
Element of the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
(0. K : ( ( ) ( ) set ) ) : ( ( ) ( )
Element of the
carrier of
K : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) #) : ( (
strict ) (
strict )
doubleLoopStr ) ;
end;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr ) holds
(
addLoopStr(# the
carrier of
(opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) , the
addF of
(opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
(opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
(opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr )
= addLoopStr(# the
carrier of
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) , the
addF of
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr ) & (
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) is
add-associative &
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) is
right_zeroed &
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) is
right_complementable implies
comp (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
(opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
(opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= comp K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) & ( for
x being ( ( ) ( )
set ) holds
(
x : ( ( ) ( )
set ) is ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) iff
x : ( ( ) ( )
set ) is ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) ) ) ) ;
begin
definition
let K be ( ( non
empty ) ( non
empty )
doubleLoopStr ) ;
let V be ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) ;
func opp V -> ( (
strict ) (
strict )
RightModStr over
opp K : ( ( ) ( )
set ) : ( (
strict ) (
strict )
doubleLoopStr ) )
means
for
o being ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like V17(
[: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) st
o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
= ~ the
lmult of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like V17(
[: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) holds
it : ( ( ) ( )
M29(
K : ( ( ) ( )
set ) ,
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
= RightModStr(# the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) , the
addF of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ,
(0. V : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( )
Element of the
carrier of
V : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) ,
o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
RightModStr over
opp K : ( ( ) ( )
set ) : ( (
strict ) (
strict )
doubleLoopStr ) ) ;
end;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
V being ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) holds
(
addLoopStr(# the
carrier of
(opp V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
(opp V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
(opp V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr )
= addLoopStr(# the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr ) & ( for
x being ( ( ) ( )
set ) holds
(
x : ( ( ) ( )
set ) is ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) iff
x : ( ( ) ( )
set ) is ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
V being ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) holds the
rmult of
(opp V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= opp the
lmult of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) ;
definition
let K be ( ( non
empty ) ( non
empty )
doubleLoopStr ) ;
let W be ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) ;
func opp W -> ( (
strict ) (
strict )
VectSpStr over
opp K : ( ( ) ( )
set ) : ( (
strict ) (
strict )
doubleLoopStr ) )
means
for
o being ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like V17(
[: the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[: the carrier of (opp K : ( ( ) ( ) set ) ) : ( ( strict ) ( strict ) doubleLoopStr ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) st
o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
= ~ the
rmult of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like V17(
[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) )
quasi_total )
Function of
[: the carrier of K : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) holds
it : ( ( ) ( )
M29(
K : ( ( ) ( )
set ) ,
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
= VectSpStr(# the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) , the
addF of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ,
(0. W : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( )
Element of the
carrier of
W : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) ) ,
o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of W : ( ( non empty ) ( non empty ) RightModStr over K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
VectSpStr over
opp K : ( ( ) ( )
set ) : ( (
strict ) (
strict )
doubleLoopStr ) ) ;
end;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
W being ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) holds
(
addLoopStr(# the
carrier of
(opp W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
(opp W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
(opp W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr )
= addLoopStr(# the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
addLoopStr ) & ( for
x being ( ( ) ( )
set ) holds
(
x : ( ( ) ( )
set ) is ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) iff
x : ( ( ) ( )
set ) is ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ) ) ) ;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
W being ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) holds the
lmult of
(opp W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= opp the
rmult of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
V being ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) )
for
o being ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of K : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
for
x being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
for
y being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
for
v being ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) )
for
w being ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
= y : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) &
v : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) )
= w : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) holds
(opp o : ( ( Function-like quasi_total ) ( non empty Relation-like [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like V17([: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) quasi_total ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) RightModStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
. (
w : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ,
y : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
= o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
. (
x : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) ,
v : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
W being ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) )
for
o being ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of K : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
for
x being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
for
y being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
for
v being ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) )
for
w being ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) )
= y : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) &
v : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) )
= w : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) holds
(opp o : ( ( Function-like quasi_total ) ( non empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) -valued Function-like V17([: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) quasi_total ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of (opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of (opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( ( strict ) ( non empty strict ) VectSpStr over opp b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
. (
y : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) ,
w : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(opp b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
= o : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
. (
v : ( ( ) ( )
Vector of ( ( ) ( non
empty )
set ) ) ,
x : ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
K being ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr )
for
V being ( ( non
empty ) ( non
empty )
VectSpStr over
K : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) holds
opp (opp V : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp (opp b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) )
= VectSpStr(# the
carrier of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) , the
lmult of
V : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) VectSpStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
VectSpStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) ;
theorem
for
K being ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr )
for
W being ( ( non
empty ) ( non
empty )
RightModStr over
K : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) holds
opp (opp W : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) ) : ( (
strict ) ( non
empty strict )
VectSpStr over
opp b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
RightModStr over
opp (opp b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) )
= RightModStr(# the
carrier of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) , the
addF of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) ) , the
rmult of
W : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like [: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty ) ( non
empty )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17(
[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
quasi_total )
Element of
bool [:[: the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RightModStr over b1 : ( ( non empty strict ) ( non empty strict ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RightModStr over
b1 : ( ( non
empty strict ) ( non
empty strict )
doubleLoopStr ) ) ;
begin
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
J being ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) holds
(
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
isomorphism iff (
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
additive & ( for
x,
y being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) holds
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
* (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (1_ K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= 1_ K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
one-to-one &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
onto ) ) ;
theorem
for
K being ( ( non
empty ) ( non
empty )
doubleLoopStr )
for
J being ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) holds
(
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
antiisomorphism iff (
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
additive & ( for
x,
y being ( ( ) ( )
Scalar of ( ( ) ( non
empty )
set ) ) holds
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
* (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (1_ K : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
= 1_ K : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
one-to-one &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty ) ( non
empty )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
onto ) ) ;
theorem
for
K,
L being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring)
for
J being ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
x,
y being ( ( ) (
right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) st
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
linear holds
(
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (0. K : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) (
V46(
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) )
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= 0. L : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) (
V46(
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) )
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (- x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= - (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
- (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
K,
L being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring)
for
J being ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
x,
y being ( ( ) (
right_complementable )
Scalar of ( ( ) ( non
empty )
set ) ) st
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
antilinear holds
(
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (0. K : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) (
V46(
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) )
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= 0. L : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) (
V46(
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) )
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (- x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= - (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) &
J : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
= (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
- (J : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) ) ) ;
begin
begin
begin
definition
let K,
L be ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ;
let J be ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
K : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-defined the
carrier of
L : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
K : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) ;
let V be ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
K : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) ;
let W be ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
L : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) ;
mode Homomorphism of
J,
V,
W -> ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
V : ( (
Function-like quasi_total ) (
Relation-like [:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
-defined the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set )
-valued Function-like V17( the
carrier of
V : ( (
Function-like quasi_total ) (
Relation-like [:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
quasi_total )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) )
means
( ( for
x,
y being ( ( ) (
right_complementable )
Vector of ( ( ) ( )
set ) ) holds
it : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
V : ( (
Function-like quasi_total ) (
Relation-like [:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) )
= (it : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) -defined J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) -valued Function-like quasi_total ) Element of bool [:[: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) )
+ (it : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) -defined J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) -valued Function-like quasi_total ) Element of bool [:[: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) ) ) & ( for
a being ( ( ) (
right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
right_complementable )
Vector of ( ( ) ( )
set ) ) holds
it : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
. (a : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
V : ( (
Function-like quasi_total ) (
Relation-like [:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set )
-defined J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) ))
-valued Function-like quasi_total )
Element of
bool [:[:J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) )
= (J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) . a : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set ) )
* (it : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) -defined J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) -valued Function-like quasi_total ) Element of bool [:[: the carrier of K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) ,J : ( ( ) ( ) M29(K : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ,L : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) )) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
W : ( ( ) ( )
Element of
J : ( ( ) ( )
M29(
K : ( ( non
empty right_complementable add-associative right_zeroed ) ( non
empty right_complementable add-associative right_zeroed )
addLoopStr ) ,
L : ( (
Relation-like Function-like ) (
Relation-like Function-like )
set ) )) ) : ( ( ) ( )
set ) ) ) );
end;
theorem
for
K being ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring)
for
V,
W being ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
K : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) )
for
f being ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) holds
(
f : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is ( ( ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Homomorphism of
V : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) ,
W : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) ) iff ( ( for
x,
y being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
+ (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) ) & ( for
a being ( ( ) (
right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) ( non
empty Relation-like the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set )
-valued Function-like V17( the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. (a : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b2 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) )
= a : ( ( ) (
right_complementable )
Scalar of ( ( ) ( non
empty )
set ) )
* (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b2 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b3 : ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
b1 : ( ( non
empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non
empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed )
Ring) ) : ( ( ) ( non
empty )
set ) ) ) ) ) ;