begin
definition
attr c1 is
strict ;
struct CLSStruct -> ( ( ) ( )
addLoopStr ) ;
aggr CLSStruct(#
carrier,
ZeroF,
addF,
Mult #)
-> ( (
strict ) (
strict )
CLSStruct ) ;
sel Mult c1 -> ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of c1 : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
c1 : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of c1 : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
c1 : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of c1 : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
c1 : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of c1 : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
c1 : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) ) ;
end;
definition
let V be ( ( non
empty ) ( non
empty )
CLSStruct ) ;
let v be ( ( ) ( )
VECTOR of
V : ( ( non
empty ) ( non
empty )
CLSStruct ) ) ;
let z be ( (
complex ) (
complex )
Complex) ;
func z * v -> ( ( ) ( )
Element of ( ( ) ( )
set ) )
equals
the
Mult of
V : ( ( ) ( )
NORMSTR ) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( ) ( )
NORMSTR ) : ( ( ) ( )
set ) )
. [z : ( ( Function-like V18([:V : ( ( ) ( ) NORMSTR ) ,V : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) NORMSTR ) ) ) ( Relation-like [:V : ( ( ) ( ) NORMSTR ) ,V : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) -defined V : ( ( ) ( ) NORMSTR ) -valued Function-like V18([:V : ( ( ) ( ) NORMSTR ) ,V : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) NORMSTR ) ) ) Element of bool [:[:V : ( ( ) ( ) NORMSTR ) ,V : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) Element of V : ( ( ) ( ) NORMSTR ) ) ] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ;
end;
registration
let ZS be ( ( non
empty ) ( non
empty )
set ) ;
let O be ( ( ) ( )
Element of
ZS : ( ( non
empty ) ( non
empty )
set ) ) ;
let F be ( (
Function-like V18(
[:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined ZS : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
ZS : ( ( non
empty ) ( non
empty )
set ) ) ;
let G be ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined ZS : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) ;
cluster CLSStruct(#
ZS : ( ( non
empty ) ( non
empty )
set ) ,
O : ( ( ) ( )
Element of
ZS : ( ( non
empty ) ( non
empty )
set ) ) ,
F : ( (
Function-like V18(
[:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined ZS : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) )
Element of
bool [:[:ZS : ( ( non empty ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
G : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined ZS : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
ZS : ( ( non
empty ) ( non
empty )
set ) ) )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty V50() ) set ) ,ZS : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) #) : ( (
strict ) (
strict )
CLSStruct )
-> non
empty strict ;
end;
definition
func Trivial-CLSStruct -> ( (
strict ) (
strict )
CLSStruct )
equals
CLSStruct(# 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ,
op0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal )
Element of 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) ,
op2 : ( (
Function-like V18(
[:1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty )
set ) ,1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) ) (
Relation-like [:1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty )
set )
-defined 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) )
-valued Function-like V18(
[:1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty )
set ) ,1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) )
Element of
bool [:[:1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(pr2 (COMPLEX : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) )) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty V50() )
set ) ,1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty V50() )
set )
-defined 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty V50() )
set ) ,1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non empty V50() ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ;
end;
begin
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ;
mode Subspace of
V -> ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace)
means
( the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
c= the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) &
0. it : ( ( ) ( )
set ) : ( ( ) ( )
Element of the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 0. V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
Element of the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) ) & the
addF of
it : ( ( ) ( )
set ) : ( (
Function-like V18(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) )
Element of
bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty ) ( non
empty )
set ) : ( (
Function-like V18(
[: the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [: the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[: the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) ) )
Element of
bool [:[: the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
|| the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) & the
Mult of
it : ( ( ) ( )
set ) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
it : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= the
Mult of
V : ( ( non
empty ) ( non
empty )
set ) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) , the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
| [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set )
-valued Function-like )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) );
end;
theorem
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace)
for
V1 being ( ( ) ( )
Subset of )
for
D being ( ( non
empty ) ( non
empty )
set )
for
d1 being ( ( ) ( )
Element of
D : ( ( non
empty ) ( non
empty )
set ) )
for
A being ( (
Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
D : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
D : ( ( non
empty ) ( non
empty )
set ) ) st
V1 : ( ( ) ( )
Subset of )
= D : ( ( non
empty ) ( non
empty )
set ) &
d1 : ( ( ) ( )
Element of
b3 : ( ( non
empty ) ( non
empty )
set ) )
= 0. V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) (
zero right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) &
A : ( (
Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
b3 : ( ( non
empty ) ( non
empty )
set ) )
= the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( (
Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
|| V1 : ( ( ) ( )
Subset of ) : ( ( ) (
Relation-like Function-like )
set ) &
M : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) )
= the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
| [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,V1 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V50() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) holds
CLSStruct(#
D : ( ( non
empty ) ( non
empty )
set ) ,
d1 : ( ( ) ( )
Element of
b3 : ( ( non
empty ) ( non
empty )
set ) ) ,
A : ( (
Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
b3 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b3 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) is ( ( ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) ;
definition
let V be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ;
func (Omega). V -> ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
Subspace of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) )
equals
CLSStruct(# the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) , the
ZeroF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) (
right_complementable )
Element of the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) , the
addF of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( (
Function-like V18(
[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) , the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) , the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ;
end;
begin
definition
let CNS be ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ;
let S be ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) ;
let z be ( (
complex ) (
complex )
Complex) ;
func z * S -> ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) )
means
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) holds
it : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) ,
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set )
-defined CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) ,
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) ) )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) )
= z : ( (
Function-like V18(
[:CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) ,
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) ) ) (
Relation-like [:CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set )
-defined CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct )
-valued Function-like V18(
[:CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) ,
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) ) )
Element of
bool [:[:CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( ) set ) ,CNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
* (S : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
CNS : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty )
set ) ) ;
end;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
S1,
S2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent &
S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) )
+ S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) is
convergent ;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
S1,
S2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent &
S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) )
- S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) is
convergent ;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
g being ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
for
S being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent &
lim S : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
= g : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) ) holds
(
||.(S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - g : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) .|| : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ,
REAL : ( ( ) ( non
empty V50() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined REAL : ( ( ) ( non
empty V50() )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ,
REAL : ( ( ) ( non
empty V50() )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ,REAL : ( ( ) ( non empty V50() ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) is
convergent &
lim ||.(S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - g : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) .|| : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ,
REAL : ( ( ) ( non
empty V50() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined REAL : ( ( ) ( non
empty V50() )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ,
REAL : ( ( ) ( non
empty V50() )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) ,REAL : ( ( ) ( non empty V50() ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V50() )
set ) )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50()
cardinal )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) ) ) ;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
S1,
S2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent &
S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
lim (S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) + S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
= (lim S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
+ (lim S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
S1,
S2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent &
S2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
lim (S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
= (lim S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
- (lim S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
x being ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
for
S being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
lim (S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( right_complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
= (lim S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
- x : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of the
carrier of
b1 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
z being ( (
complex ) (
complex )
Complex)
for
CNS being ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace)
for
S being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) st
S : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) is
convergent holds
lim (z : ( ( complex ) ( complex ) Complex) * S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V50()
cardinal limit_cardinal )
Element of
bool REAL : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like )
ComplexNormSpace) : ( ( ) ( non
empty )
set ) ) )
sequence of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) )
= z : ( (
complex ) (
complex )
Complex)
* (lim S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty V50() ) set ) : ( ( ) ( non empty V50() ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
right_complementable )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty )
set ) ) ;
theorem
for
z being ( (
complex ) (
complex )
Complex)
for
D being ( ( non
empty ) ( non
empty )
set )
for
d1 being ( ( ) ( )
Element of
D : ( ( non
empty ) ( non
empty )
set ) )
for
A being ( (
Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
D : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
D : ( ( non
empty ) ( non
empty )
set ) )
for
V being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace)
for
V1 being ( ( ) ( )
Subset of )
for
v being ( ( ) (
right_complementable )
VECTOR of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) )
for
w being ( ( ) ( )
VECTOR of
CLSStruct(#
D : ( ( non
empty ) ( non
empty )
set ) ,
d1 : ( ( ) ( )
Element of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
A : ( (
Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ) st
V1 : ( ( ) ( )
Subset of )
= D : ( ( non
empty ) ( non
empty )
set ) &
M : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) )
= the
Mult of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) , the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
| [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,V1 : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined the
carrier of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V50() ) set ) , the carrier of b6 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) : ( ( ) ( non
empty V50() )
set ) ) &
w : ( ( ) ( )
VECTOR of
CLSStruct(#
b2 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( ) ( )
Element of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
b4 : ( (
Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
b5 : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) )
= v : ( ( ) (
right_complementable )
VECTOR of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) holds
z : ( (
complex ) (
complex )
Complex)
* w : ( ( ) ( )
VECTOR of
CLSStruct(#
b2 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( ) ( )
Element of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
b4 : ( (
Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
BinOp of
b2 : ( ( non
empty ) ( non
empty )
set ) ) ,
b5 : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like V18(
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) )
Function of
[:COMPLEX : ( ( ) ( non empty V50() ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty V50() )
set ) ,
b2 : ( ( non
empty ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ) : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= z : ( (
complex ) (
complex )
Complex)
* v : ( ( ) (
right_complementable )
VECTOR of
b6 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) : ( ( ) (
right_complementable )
Element of ( ( ) ( non
empty )
set ) ) ;