begin
definition
let V be ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
let W1,
W2 be ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ;
func W1 + W2 -> ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
V : ( ( ) ( )
UNITSTR ) )
means
the
carrier of
it : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
UNITSTR )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
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 : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) where v, u is ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) : ( v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( Function-like V18([:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) ) ) ( Relation-like [:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) -defined V : ( ( ) ( ) UNITSTR ) -valued Function-like V18([:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) ) ) Element of bool [:[:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) } ;
end;
definition
let V be ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
let W1,
W2 be ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ;
func W1 /\ W2 -> ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
V : ( ( ) ( )
UNITSTR ) )
means
the
carrier of
it : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
UNITSTR )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= the
carrier of
W1 : ( ( ) ( )
Element of
V : ( ( ) ( )
UNITSTR ) ) : ( ( ) ( )
set )
/\ the
carrier of
W2 : ( (
Function-like V18(
[:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) ) (
Relation-like [:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( ) ( )
UNITSTR )
-valued Function-like V18(
[:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( ) ( )
UNITSTR ) ) )
Element of
bool [:[:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) ;
end;
begin
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
(
((0). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ ((Omega). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) &
((Omega). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ ((0). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) ) ;
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace)
for
W being ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) holds
(
((Omega). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ W : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) &
W : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ ((Omega). V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) ) ;
begin
begin
definition
let V be ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
let W1,
W2 be ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ;
pred V is_the_direct_sum_of W1,
W2 means
(
UNITSTR(# the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) , the
ZeroF of
V : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
V : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) , the
U7 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 ) ) , the
scalar of
V : ( ( ) ( )
set ) : ( (
Function-like V18(
[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
UNITSTR )
= 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
V : ( ( ) ( )
set ) )
= (0). V : ( ( ) ( )
set ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
V : ( ( ) ( )
set ) ) );
end;
begin
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace)
for
W being ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
for
L being ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Linear_Compl of
W : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ) holds
(
W : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ L : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Linear_Compl of
b2 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) &
L : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Linear_Compl of
b2 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) )
+ W : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) ) ;
begin
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace)
for
W1,
W2 being ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) holds
(
W1 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
+ W2 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) &
v2 : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
in W2 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) &
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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) ) ;
definition
let V be ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
let v be ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) ;
let W1,
W2 be ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ;
assume
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace)
is_the_direct_sum_of W1 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ,
W2 : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
;
func v |-- (
W1,
W2)
-> ( ( ) ( )
Element of
[: the carrier of V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) )
means
(
v : ( ( ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) )
= (it : ( ( Function-like V18([:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ) ) ( Relation-like [:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) -defined K93() : ( ( ) ( V33() V34() V35() V39() ) set ) -valued Function-like V18([:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ) ) Element of bool [:[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) )
+ (it : ( ( Function-like V18([:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ) ) ( Relation-like [:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) -defined K93() : ( ( ) ( V33() V34() V35() V39() ) set ) -valued Function-like V18([:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ) ) Element of bool [:[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) &
it : ( (
Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) )
`1 : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) )
in W1 : ( (
Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) ) ) (
Relation-like [:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR )
-valued Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) ) )
Element of
bool [:[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) &
it : ( (
Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[:V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) )
`2 : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) )
in W2 : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set )
-defined V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) ,
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) );
end;
begin
begin
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
cluster LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
LattStr )
-> strict Lattice-like ;
end;
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) holds
LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( (
Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ,(Subspaces b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( 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 V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ;
cluster LattStr(#
(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non
empty )
set ) ,
(SubJoin V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ,
(SubMeet V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( (
Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) ,(Subspaces V : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( non
empty )
set ) ) )
BinOp of
Subspaces V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
UNITSTR ) : ( ( ) ( 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;
begin
theorem
for
V being ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace)
for
W being ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) st ( for
v being ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) ) holds
v : ( ( ) ( )
VECTOR of ( ( ) ( non
empty )
set ) )
in W : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) ) ) holds
W : ( (
strict ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like )
Subspace of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) )
= UNITSTR(# the
carrier of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) , the
U7 of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set )
-defined the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) , the
carrier of
b1 : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[:K93() : ( ( ) ( V33() V34() V35() V39() ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) , the
scalar of
V : ( ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non
empty V99()
Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like )
RealUnitarySpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) ,
K93() : ( ( ) (
V33()
V34()
V35()
V39() )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ,K93() : ( ( ) ( V33() V34() V35() V39() ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
UNITSTR ) ;