begin
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
let W1,
W2 be ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ;
func W1 + W2 -> ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( ) ( )
RLSStruct ) )
means
the
carrier of
it : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
RLSStruct )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= { (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) where v, u is ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) : ( v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( Function-like V18([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) ( Relation-like [:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) -defined V : ( ( ) ( ) RLSStruct ) -valued Function-like V18([:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) ) ) Element of bool [:[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) } ;
end;
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
let W1,
W2 be ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ;
func W1 /\ W2 -> ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( ) ( )
RLSStruct ) )
means
the
carrier of
it : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
RLSStruct )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= the
carrier of
W1 : ( ( ) ( )
Element of
V : ( ( ) ( )
RLSStruct ) ) : ( ( ) ( )
set )
/\ the
carrier of
W2 : ( (
Function-like V18(
[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) ) (
Relation-like [:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
RLSStruct )
-valued Function-like V18(
[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
RLSStruct ) ) )
Element of
bool [:[:V : ( ( ) ( ) RLSStruct ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) ;
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
(
((0). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ ((Omega). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) &
((Omega). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ ((0). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) ) ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace)
for
W being ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) holds
(
((Omega). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ W : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) &
W : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ ((Omega). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) ) ;
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
let W1,
W2 be ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ;
pred V is_the_direct_sum_of W1,
W2 means
(
RLSStruct(# the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) , the
ZeroF of
V : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) , the
addF of
V : ( ( ) ( )
set ) : ( (
Function-like V18(
[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) )
Element of
bool [:[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( ) ( )
set ) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
RLSStruct )
= W1 : ( ( ) ( )
set )
+ W2 : ( (
Function-like V18(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
set ) ) ) (
Relation-like [:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
set )
-valued Function-like V18(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
set ) ) )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( ) ( )
set ) ) &
W1 : ( ( ) ( )
set )
/\ W2 : ( (
Function-like V18(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
set ) ) ) (
Relation-like [:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
set )
-valued Function-like V18(
[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
set ) ) )
Element of
bool [:[:V : ( ( ) ( ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( ) ( )
set ) )
= (0). V : ( ( ) ( )
set ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( ) ( )
set ) ) );
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace)
for
W being ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
for
L being ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Linear_Compl of
W : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ) holds
(
W : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ L : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Linear_Compl of
b2 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) &
L : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Linear_Compl of
b2 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) )
+ W : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) ) ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace)
for
W1,
W2 being ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) holds
(
W1 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
+ W2 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) iff for
v being ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) ex
v1,
v2 being ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) st
(
v1 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
in W1 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) &
v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
in W2 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) &
v : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
= v1 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
+ v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) ;
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
let v be ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) ;
let W1,
W2 be ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ;
assume
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace)
is_the_direct_sum_of W1 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ,
W2 : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
;
func v |-- (
W1,
W2)
-> ( ( ) ( )
Element of
[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) )
means
(
v : ( ( ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) )
= (it : ( ( ) ( ) Element of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) `1) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) )
+ (it : ( ( ) ( ) Element of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) `2) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) &
it : ( ( ) ( )
Element of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) )
`1 : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) )
in W1 : ( (
Function-like V18(
[:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) ) ) (
Relation-like [:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct )
-valued Function-like V18(
[:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) ) )
Element of
bool [:[:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) &
it : ( ( ) ( )
Element of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) )
`2 : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) )
in W2 : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) );
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
LattStr ) is ( ( non
empty Lattice-like ) ( non
empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
Lattice) ;
registration
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
cluster LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
LattStr )
-> strict Lattice-like ;
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr ) is
lower-bounded ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr ) is
upper-bounded ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr ) is ( ( non
empty Lattice-like V77() ) ( non
empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V77() )
01_Lattice) ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr ) is
modular ;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) holds
LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr ) is
complemented ;
registration
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ;
cluster LattStr(#
(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RLSStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RLSStruct ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like )
LattStr )
-> strict modular lower-bounded upper-bounded complemented ;
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace)
for
W being ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) st ( for
v being ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
v : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
in W : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) ) ) holds
W : ( (
strict ) ( non
empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
Subspace of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) )
= RLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() )
RealLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
RLSStruct ) ;