begin
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let Y 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 FuncExtMult (
X,
Y)
-> ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) )
means
for
c being ( (
complex ) (
complex )
Complex)
for
f being ( ( ) (
Relation-like X : ( ( ) ( )
CNORMSTR )
-defined the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) )
for
x being ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) holds
(it : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . [c : ( ( complex ) ( complex ) Complex) ,f : ( ( ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( 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 total quasi_total ) Element of Funcs (X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( 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 functional ) FUNCTION_DOMAIN of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( 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 ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) ( )
set )
. x : ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= c : ( (
complex ) (
complex )
Complex)
* (f : ( ( ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined the carrier of Y : ( ( 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 total quasi_total ) Element of Funcs (X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( 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 functional ) FUNCTION_DOMAIN of X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( 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 ) ) ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) ;
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
h,
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
for
a being ( (
complex ) (
complex )
Complex) holds
(
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= (FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. [a : ( ( complex ) ( complex ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) iff for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
= a : ( (
complex ) (
complex )
Complex)
* (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) holds
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= (FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f,
g,
h being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) holds
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
((FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Element of bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ,h : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= (FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
((FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Element of bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ,g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) holds
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
(FuncZero (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) holds
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
((FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Function of [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) . [(- 1r : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= FuncZero (
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( 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) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) holds
(FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. [1r : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
= f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
for
a,
b being ( (
complex ) (
complex )
Complex) holds
(FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. [a : ( ( complex ) ( complex ) Complex) ,((FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Function of [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) . [b : ( ( complex ) ( complex ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) ] : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set )
= (FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. [(a : ( ( complex ) ( complex ) Complex) * b : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
for
a,
b being ( (
complex ) (
complex )
Complex) holds
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. (
((FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Function of [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) . [a : ( ( complex ) ( complex ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) (
Relation-like Function-like )
set ) ,
((FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total Function-yielding V34() ) Function of [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) . [b : ( ( complex ) ( complex ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) (
Relation-like Function-like )
set ) ) : ( ( ) ( )
set )
= (FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) )
. [(a : ( ( complex ) ( complex ) Complex) + b : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( )
set ) : ( ( ) (
Relation-like Function-like )
set ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y 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) holds
CLSStruct(#
(Funcs (X : ( ( non empty ) ( non empty ) set ) , the carrier of Y : ( ( 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 functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ,
(FuncZero (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) ) ,
(FuncAdd (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(FuncExtMult (X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( 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 quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) : ( ( ) ( 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 ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ;
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let Y 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 ComplexVectSpace (
X,
Y)
-> ( ( 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)
equals
CLSStruct(#
(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) ,
(FuncZero (X : ( ( ) ( ) CNORMSTR ) ,Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) )) : ( ( ) (
Relation-like X : ( ( ) ( )
CNORMSTR )
-defined the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set )
-valued Function-like total quasi_total )
Element of
Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) ) ,
(FuncAdd (X : ( ( ) ( ) CNORMSTR ) ,Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non empty ) set ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(FuncExtMult (X : ( ( ) ( ) CNORMSTR ) ,Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set )
-defined Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) )
-valued Function-like total quasi_total Function-yielding V34() )
Function of
[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(Funcs (X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) )) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of X : ( ( ) ( ) CNORMSTR ) , the carrier of Y : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) :] : ( ( ) ( non
empty )
set ) ,
Funcs (
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
X : ( ( ) ( )
CNORMSTR ) , the
carrier of
Y : ( ( ) ( )
Element of
X : ( ( ) ( )
CNORMSTR ) ) : ( ( ) ( )
set ) ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ;
end;
begin
theorem
for
X,
Y 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) holds
CLSStruct(#
(LinearOperators (X : ( ( 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) ,Y : ( ( 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 functional )
Subset of ) ,
(Zero_ ((LinearOperators (X : ( ( 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) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) (
Relation-like Function-like )
Element of
LinearOperators (
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) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) : ( ( ) ( non
empty functional )
Subset of ) ) ,
(Add_ ((LinearOperators (X : ( ( 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) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined LinearOperators (
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) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) : ( ( ) ( non
empty functional )
Subset of )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((LinearOperators (X : ( ( 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) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined LinearOperators (
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) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) : ( ( ) ( non
empty functional )
Subset of )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(LinearOperators (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) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( non empty functional ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( 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
ComplexVectSpace ( the
carrier of
X : ( ( 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 ) ,
Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) ;
registration
let X,
Y 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) ;
cluster CLSStruct(#
(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional )
Subset of ) ,
(Zero_ ((LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) (
Relation-like Function-like )
Element of
LinearOperators (
X : ( ( 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 ) ,
Y : ( ( 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 functional )
Subset of ) ) ,
(Add_ ((LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined LinearOperators (
X : ( ( 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 ) ,
Y : ( ( 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 functional )
Subset of )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( 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 ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined LinearOperators (
X : ( ( 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 ) ,
Y : ( ( 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 functional )
Subset of )
-valued Function-like total quasi_total Function-yielding V34() )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(LinearOperators (X : ( ( 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 ) ,Y : ( ( 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 functional ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct )
-> right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;
definition
let X,
Y 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 C_VectorSpace_of_LinearOperators (
X,
Y)
-> ( ( 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)
equals
CLSStruct(#
(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( )
Subset of ) ,
(Zero_ ((LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( non empty ) ( non empty ) CLSStruct ) : ( ( ) ( non empty ) set ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( )
Element of
LinearOperators (
X : ( ( non
empty ) ( non
empty )
CLSStruct ) ,
Y : ( ( 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 ) ) : ( ( ) ( )
Subset of ) ) ,
(Add_ ((LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( non empty ) ( non empty ) CLSStruct ) : ( ( ) ( non empty ) set ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) (
Relation-like [:(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined LinearOperators (
X : ( ( non
empty ) ( non
empty )
CLSStruct ) ,
Y : ( ( 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 ) ) : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
Element of
bool [:[:(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) ,(ComplexVectSpace ( the carrier of X : ( ( non empty ) ( non empty ) CLSStruct ) : ( ( ) ( non empty ) set ) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set )
-defined LinearOperators (
X : ( ( non
empty ) ( non
empty )
CLSStruct ) ,
Y : ( ( 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 ) ) : ( ( ) ( )
Subset of )
-valued Function-like quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) ,(LinearOperators (X : ( ( non empty ) ( non empty ) CLSStruct ) ,Y : ( ( 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 ) )) : ( ( ) ( ) Subset of ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
CLSStruct ) ;
end;
begin
theorem
for
X,
Y 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) holds
CLSStruct(#
(BoundedLinearOperators (X : ( ( 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) ,Y : ( ( 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 )
Subset of ) ,
(Zero_ ((BoundedLinearOperators (X : ( ( 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) ,Y : ( ( 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 ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( )
Element of
BoundedLinearOperators (
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) ,
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 )
Subset of ) ) ,
(Add_ ((BoundedLinearOperators (X : ( ( 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) ,Y : ( ( 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 ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedLinearOperators (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) ,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 ) Subset of ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
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) ,
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 )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:(BoundedLinearOperators (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) ,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 ) Subset of ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((BoundedLinearOperators (X : ( ( 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) ,Y : ( ( 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 ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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) ,Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
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) ,
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 )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (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) ,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 ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( 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
C_VectorSpace_of_LinearOperators (
X : ( ( 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) ,
Y : ( ( 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital )
ComplexLinearSpace) ) ;
registration
let X,
Y be ( ( 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) ;
cluster CLSStruct(#
(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non
empty )
Subset of ) ,
(Zero_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( )
Element of
BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) ) ,
(Add_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct )
-> right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
end;
definition
let X,
Y be ( ( 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) ;
func C_VectorSpace_of_BoundedLinearOperators (
X,
Y)
-> ( ( 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)
equals
CLSStruct(#
(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non
empty )
Subset of ) ,
(Zero_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( )
Element of
BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) ) ,
(Add_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital )
CLSStruct ) ;
end;
definition
let X,
Y be ( ( 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) ;
func BoundedLinearOperatorsNorm (
X,
Y)
-> ( (
Function-like quasi_total ) ( non
empty Relation-like BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-defined REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set )
-valued Function-like total quasi_total V132()
V133()
V134() )
Function of
BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) ,
REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set ) )
means
for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) holds
it : ( (
Function-like quasi_total ) (
Relation-like [:X : ( ( 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 ) CNORMSTR ) ,X : ( ( 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 ) CNORMSTR ) :] : ( ( ) ( )
set )
-defined X : ( ( 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 )
CNORMSTR )
-valued Function-like quasi_total )
Element of
bool [:[:X : ( ( 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 ) CNORMSTR ) ,X : ( ( 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 ) CNORMSTR ) :] : ( ( ) ( ) set ) ,X : ( ( 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 ) CNORMSTR ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
set ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set ) )
= upper_bound (PreNorms (modetrans (x : ( ( ) ( ) set ) ,X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( Function-like quasi_total additive homogeneous Lipschitzian ) ( non empty Relation-like the carrier of X : ( ( 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 ) CNORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( 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 ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total additive homogeneous Lipschitzian ) LinearOperator of X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) ) ) : ( ( non
empty ) ( non
empty V142()
V143()
V144() )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set ) ) ;
end;
definition
let X,
Y be ( ( 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) ;
func C_NormSpace_of_BoundedLinearOperators (
X,
Y)
-> ( ( non
empty ) ( non
empty )
CNORMSTR )
equals
CNORMSTR(#
(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non
empty )
Subset of ) ,
(Zero_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( ( ) ( )
Element of
BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) ) ,
(Add_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(Mult_ ((BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) ,(C_VectorSpace_of_LinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( 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 constituted-Functions strict vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like [:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set )
-defined BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-valued Function-like total quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V35() V142() V148() ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(BoundedLinearOperators (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( ( ) ( non empty ) Subset of ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ,
(BoundedLinearOperatorsNorm (X : ( ( 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 ) CNORMSTR ) ,Y : ( ( 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 ) CNORMSTR ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of )
-defined REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set )
-valued Function-like total quasi_total V132()
V133()
V134() )
Function of
BoundedLinearOperators (
X : ( ( 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 )
CNORMSTR ) ,
Y : ( ( 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 )
CNORMSTR ) ) : ( ( ) ( non
empty )
Subset of ) ,
REAL : ( ( ) ( non
empty V35()
V142()
V143()
V144()
V148() )
set ) ) #) : ( (
strict ) ( non
empty strict )
CNORMSTR ) ;
end;
begin