begin
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func ComplexFuncAdd A -> ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
means
for
f,
g being ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
it : ( ( ) ( )
VectSpStr over
A : ( ( ) ( )
CNORMSTR ) )
. (
f : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= addcomplex : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
.: (
f : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
end;
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func ComplexFuncMult A -> ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
means
for
f,
g being ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
it : ( ( ) ( )
VectSpStr over
A : ( ( ) ( )
CNORMSTR ) )
. (
f : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= multcomplex : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
bool [:[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
.: (
f : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like A : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
end;
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func ComplexFuncExtMult A -> ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
means
for
z being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
for
f being ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
for
x being ( ( ) ( )
Element of
A : ( ( ) ( )
CNORMSTR ) ) holds
(it : ( ( ) ( ) VectSpStr over A : ( ( ) ( ) CNORMSTR ) ) . [z : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (A : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. x : ( ( ) ( )
Element of
A : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
* (f : ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (A : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ;
end;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
h,
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) iff for
x being ( ( ) ( )
Element of
A : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
+ (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
h,
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) iff for
x being ( ( ) ( )
Element of
A : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
* (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
h,
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
for
a being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) holds
(
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) iff for
x being ( ( ) ( )
Element of
A : ( ( non
empty ) ( non
empty )
set ) ) holds
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= a : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
* (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,h : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,h : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
h : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
(ComplexFuncUnit A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
(ComplexFuncZero A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [(- 1r : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= ComplexFuncZero A : ( ( non
empty ) ( non
empty )
set ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [1r : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
for
a,
b being ( (
V21() ) (
V21() )
Complex) holds
(ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [a : ( ( V21() ) ( V21() ) Complex) ,((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( V21() ) ( V21() ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( )
set ) : ( ( ) ( )
set )
= (ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [(a : ( ( V21() ) ( V21() ) Complex) * b : ( ( V21() ) ( V21() ) Complex) ) : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
for
a,
b being ( (
V21() ) (
V21() )
Complex) holds
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( V21() ) ( V21() ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( V21() ) ( V21() ) Complex) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set )
= (ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [(a : ( ( V21() ) ( V21() ) Complex) + b : ( ( V21() ) ( V21() ) Complex) ) : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g,
h being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
f : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,h : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,h : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
for
a being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) holds
(ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
g : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,((ComplexFuncMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) BinOp of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . (f : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,g : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) )) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( )
Element of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b1 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
begin
theorem
for
x1 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set ) ex
f,
g being ( ( ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
( ( for
z being ( ( ) ( )
set ) st
z : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) ( )
set )
= x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) ( )
set ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) & (
z : ( ( ) ( )
set )
<> x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) ( )
set ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) ) ) & ( for
z being ( ( ) ( )
set ) st
z : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) ( )
set )
= x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) ( )
set ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) & (
z : ( ( ) ( )
set )
<> x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b2 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) ( )
set ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) ) ) ;
theorem
for
x1,
x2 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
x1 : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) &
x2 : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) &
x1 : ( ( ) ( )
set )
<> x2 : ( ( ) ( )
set ) & ( for
z being ( ( ) ( )
set ) st
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) & (
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
<> x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) ) ) & ( for
z being ( ( ) ( )
set ) st
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) & (
z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
<> x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) ) holds
for
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= ComplexFuncZero A : ( ( non
empty ) ( non
empty )
set ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(
a : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= 0c : ( ( ) (
empty V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) &
b : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= 0c : ( ( ) (
empty V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
x1,
x2 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set ) st
x1 : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) &
x2 : ( ( ) ( )
set )
in A : ( ( non
empty ) ( non
empty )
set ) &
x1 : ( ( ) ( )
set )
<> x2 : ( ( ) ( )
set ) holds
ex
f,
g being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
for
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= ComplexFuncZero A : ( ( non
empty ) ( non
empty )
set ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(
a : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) &
b : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) ;
theorem
for
x1,
x2 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
A : ( ( non
empty ) ( non
empty )
set )
= {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) } : ( ( ) ( non
empty )
set ) &
x1 : ( ( ) ( )
set )
<> x2 : ( ( ) ( )
set ) & ( for
z being ( ( ) ( )
set ) st
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) & (
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
<> x1 : ( ( ) ( )
set ) implies
f : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) ) ) & ( for
z being ( ( ) ( )
set ) st
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
in A : ( ( non
empty ) ( non
empty )
set ) holds
( (
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) : ( ( ) ( )
set )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) & (
z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
<> x1 : ( ( ) ( )
set ) implies
g : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. z : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) : ( ( ) ( )
set )
= 1r : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) ) holds
for
h being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ex
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
h : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
x1,
x2 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set ) st
A : ( ( non
empty ) ( non
empty )
set )
= {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) } : ( ( ) ( non
empty )
set ) &
x1 : ( ( ) ( )
set )
<> x2 : ( ( ) ( )
set ) holds
ex
f,
g being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
for
h being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ex
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
h : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ;
theorem
for
x1,
x2 being ( ( ) ( )
set )
for
A being ( ( non
empty ) ( non
empty )
set ) st
A : ( ( non
empty ) ( non
empty )
set )
= {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) } : ( ( ) ( non
empty )
set ) &
x1 : ( ( ) ( )
set )
<> x2 : ( ( ) ( )
set ) holds
ex
f,
g being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) st
( ( for
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
(ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= ComplexFuncZero A : ( ( non
empty ) ( non
empty )
set ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) holds
(
a : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) &
b : ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
= 0 : ( ( ) (
empty )
Element of
NAT : ( ( ) ( )
Element of
bool REAL : ( ( ) ( non
empty V37() )
set ) : ( ( ) ( )
set ) ) ) ) ) & ( for
h being ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ex
a,
b being ( ( ) (
V21() )
Element of
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) st
h : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
= (ComplexFuncAdd A : ( ( non empty ) ( non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) )
. (
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [a : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,f : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
((ComplexFuncExtMult A : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) -defined Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) -valued Function-like quasi_total ) Function of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) , Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) . [b : ( ( ) ( V21() ) Element of COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,g : ( ( ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V37() ) set ) -valued Function-like quasi_total ) Element of Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ) ] : ( ( ) ( ) Element of [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (b3 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b3 : ( ( non empty ) ( non empty ) set ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) : ( ( ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
b3 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ) ) ;
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func ComplexVectSpace A -> ( ( non
empty strict ) ( non
empty strict )
CLSStruct )
equals
CLSStruct(#
(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ,
(ComplexFuncZero A : ( ( ) ( ) CNORMSTR ) ) : ( ( ) (
Relation-like A : ( ( ) ( )
CNORMSTR )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncAdd A : ( ( ) ( ) CNORMSTR ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncExtMult A : ( ( ) ( ) CNORMSTR ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( ) ( ) CNORMSTR ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( ) ( ) CNORMSTR ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( ) ( )
CNORMSTR ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) #) : ( (
strict ) ( non
empty strict )
CLSStruct ) ;
end;
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func CRing A -> ( ( ) ( )
doubleLoopStr )
equals
doubleLoopStr(#
(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ,
(ComplexFuncAdd A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncMult A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncUnit A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( ( ) (
Relation-like A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncZero A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( ( ) (
Relation-like A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) #) : ( (
strict ) ( non
empty strict )
doubleLoopStr ) ;
end;
definition
let A be ( ( non
empty ) ( non
empty )
set ) ;
func CAlgebra A -> ( (
strict ) (
strict )
ComplexAlgebraStr )
equals
ComplexAlgebraStr(#
(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ,
(ComplexFuncMult A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncAdd A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( (
Function-like quasi_total ) (
Relation-like [:(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
BinOp of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncExtMult A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( (
Function-like quasi_total ) (
Relation-like [:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set )
-defined Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) )
-valued Function-like quasi_total )
Function of
[:COMPLEX : ( ( ) ( non empty V37() ) set ) ,(Funcs (A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,COMPLEX : ( ( ) ( non empty V37() ) set ) )) : ( ( ) ( non empty ) FUNCTION_DOMAIN of A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-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 ) , COMPLEX : ( ( ) ( non empty V37() ) set ) ) :] : ( ( ) ( )
set ) ,
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncUnit A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( ( ) (
Relation-like A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) ,
(ComplexFuncZero A : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) CLSStruct ) ) : ( ( ) (
Relation-like A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 )
-defined COMPLEX : ( ( ) ( non
empty V37() )
set )
-valued Function-like quasi_total )
Element of
Funcs (
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) : ( ( ) ( non
empty )
FUNCTION_DOMAIN of
A : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-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 ) ,
COMPLEX : ( ( ) ( non
empty V37() )
set ) ) ) #) : ( (
strict ) (
strict )
ComplexAlgebraStr ) ;
end;