begin
theorem
for
K being ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr )
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) )
for
W1,
W2 being ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) st
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) )
is_the_direct_sum_of W1 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ,
W2 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) holds
for
v,
v1,
v2 being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) ) st
v : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
|-- (
W1 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ,
W2 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( ) ( )
Element of
[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) )
= [v1 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non
empty )
Element of
[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) ) holds
v : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
|-- (
W2 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ,
W1 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( ) ( )
Element of
[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) )
= [v2 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ,v1 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non
empty )
Element of
[: the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) ) ;
theorem
for
K being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field)
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) )
for
v being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
for
X being ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
for
y being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
for
W being ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
X : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) st
v : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
= y : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) ) &
X : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
= W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) & not
v : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
in X : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) holds
for
w1,
w2 being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
for
x1,
x2 being ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty non
trivial )
set ) ) st
w1 : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
|-- (
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ,
(Lin {y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ) : ( ( ) ( )
Element of
[: the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) )
= [x1 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ,(r1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non
empty )
Element of
[: the carrier of b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) ) &
w2 : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
|-- (
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ,
(Lin {y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ) : ( ( ) ( )
Element of
[: the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) )
= [x2 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ,(r2 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non
empty )
Element of
[: the carrier of b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) ) holds
(w1 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) + w2 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
(b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( ( ) ( non
empty )
set ) )
|-- (
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ,
(Lin {y : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b4 : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
+ (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ) : ( ( ) ( )
Element of
[: the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of (b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) + (Lin {b3 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) } : ( ( ) ( trivial V29() ) Element of bool the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) )
= [(x1 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) + x2 : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) ) ,((r1 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) + r2 : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) : ( ( ) ( non empty non trivial ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non
empty )
Element of
[: the carrier of b4 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) Field) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
V1() non
empty )
set ) ) ;
begin
definition
let K be ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ;
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ;
let W be ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ;
func addCoset (
V,
W)
-> ( (
Function-like quasi_total ) (
V1()
V4(
[:(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
V5(
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
Function-like non
empty V14(
[:(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
quasi_total )
BinOp of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
means
for
A,
B being ( ( ) ( )
Element of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
for
a,
b being ( ( ) (
right_complementable )
Vector of ( ( ) ( )
set ) ) st
A : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
= a : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
+ W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) &
B : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
= b : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
+ W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) holds
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) )
. (
A : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) ,
B : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) ) : ( ( ) ( )
Element of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
= (a : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) + b : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
+ W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ;
end;
definition
let K be ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ;
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ;
let W be ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ;
func lmultCoset (
V,
W)
-> ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
V5(
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
Function-like non
empty V14(
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
quasi_total )
Function of
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) ,
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
means
for
z being ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty non
trivial )
set ) )
for
A being ( ( ) ( )
Element of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
for
a being ( ( ) (
right_complementable )
Vector of ( ( ) ( )
set ) ) st
A : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
= a : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty )
set ) )
+ W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) holds
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) )
. (
z : ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty )
set ) ) ,
A : ( ( ) ( )
Element of
CosetSet (
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
W : ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) ) : ( ( ) ( )
Element of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
= (z : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * a : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
+ W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ;
end;
definition
let K be ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ;
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ;
let W be ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ;
func VectQuot (
V,
W)
-> ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non
empty non
degenerated non
trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital )
doubleLoopStr ) )
means
( the
carrier of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( ( ) ( )
set )
= CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) & the
addF of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5( the
carrier of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) )
= addCoset (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total ) (
V1()
V4(
[:(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
V5(
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
Function-like non
empty V14(
[:(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
quasi_total )
BinOp of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) &
0. it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= zeroCoset (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) & the
lmult of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5( the
carrier of
it : ( ( ) ( )
Element of
V : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) )
= lmultCoset (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
V5(
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) )
Function-like non
empty V14(
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) )
quasi_total )
Function of
[: the carrier of K : ( ( non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital ) ( non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,(CosetSet (V : ( ( ) ( ) set ) ,W : ( ( Function-like quasi_total ) ( V1() V4([:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(V : ( ( ) ( ) set ) ) Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( non empty ) ( non empty ) Subset-Family of ) :] : ( ( ) (
V1() non
empty )
set ) ,
CosetSet (
V : ( ( ) ( )
set ) ,
W : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( ) ( )
set ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( non
empty ) ( non
empty )
Subset-Family of ) ) );
end;
begin
definition
let K be ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ;
let V be ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ;
let v be ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty non
trivial )
set ) ) ;
let W be ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Linear_Compl of
Lin {v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty non trivial ) set ) ) } : ( ( ) (
trivial V29() )
Element of
bool the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) : ( ( ) ( non
empty non
trivial )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) ) ) ;
assume
v : ( ( ) (
right_complementable )
Vector of ( ( ) ( non
empty non
trivial )
set ) )
<> 0. V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) : ( ( ) (
V48(
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) )
right_complementable )
Element of the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
Field) ) : ( ( ) ( non
empty non
trivial )
set ) )
;
func coeffFunctional (
v,
W)
-> ( (
Function-like V8() non
trivial quasi_total additive homogeneous ) (
V1()
V4( the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty non
trivial )
set ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like V8() non
empty non
trivial V14( the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty non
trivial )
set ) )
quasi_total additive homogeneous 0-preserving )
linear-Functional of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
means
(
it : ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) ( V1() ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) )
. v : ( (
Function-like quasi_total ) (
V1()
V4(
[:V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
Function-like quasi_total )
Element of
bool [:[:V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) ( V1() ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
= 1_ K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) (
right_complementable )
Element of the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) ) &
it : ( (
Function-like quasi_total ) (
V1()
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
Function-like quasi_total )
Element of
bool [:[: the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) ( V1() ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) )
| the
carrier of
W : ( ( ) ( )
Element of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) : ( ( ) ( )
set ) : ( ( ) (
V1()
V4( the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty non
trivial )
set ) )
V4( the
carrier of
W : ( ( ) ( )
Element of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) : ( ( ) ( )
set ) )
V4(
[: the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ,V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) :] : ( ( ) (
V1() )
set ) )
V5(
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like )
Element of
bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) (
V1() non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= 0Functional W : ( ( ) ( )
Element of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) : ( (
Function-like quasi_total ) (
V1()
V4( the
carrier of
W : ( ( ) ( )
Element of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) : ( ( ) ( )
set ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like V14( the
carrier of
W : ( ( ) ( )
Element of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) : ( ( ) ( )
set ) )
quasi_total )
Element of
bool [: the carrier of W : ( ( ) ( ) Element of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) : ( ( ) ( ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( non
empty )
set ) ) );
end;
begin
definition
let K be ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ;
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ;
let f be ( (
Function-like quasi_total additive homogeneous ) (
V1()
V4( the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty V14( the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
quasi_total additive homogeneous 0-preserving )
linear-Functional of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non
empty right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ;
func CQFunctional f -> ( (
Function-like quasi_total additive homogeneous ) (
V1()
V4( the
carrier of
(VectQuot (V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) )) : ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like non
empty V14( the
carrier of
(VectQuot (V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) )) : ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
quasi_total additive homogeneous 0-preserving )
linear-Functional of
VectQuot (
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ,
(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non
empty strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) )
equals
QFunctional (
f : ( (
Function-like quasi_total 0-preserving ) (
V1()
V4( the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty non
trivial )
set ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like non
empty V14( the
carrier of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty non
trivial )
set ) )
quasi_total 0-preserving )
Element of
bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) (
V1() non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non
empty strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty non
trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) ) ) : ( (
Function-like quasi_total additive ) (
V1()
V4( the
carrier of
(VectQuot (V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) )) : ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) : ( ( ) ( non
empty non
trivial )
set ) )
Function-like non
empty V14( the
carrier of
(VectQuot (V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ,(Ker f : ( ( Function-like quasi_total 0-preserving ) ( V1() V4( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) V5( the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) Function-like non empty V14( the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) ) quasi_total 0-preserving ) Element of bool [: the carrier of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) : ( ( ) ( non empty non trivial ) set ) , the carrier of K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) :] : ( ( ) ( V1() non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSpStr over K : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) ) )) : ( ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSpStr over
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non
empty non
degenerated non
trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital )
doubleLoopStr ) ) : ( ( ) ( non
empty )
set ) )
quasi_total additive 0-preserving )
Functional of ( ( ) ( non
empty )
set ) ) ;
end;