begin
theorem
for
x1,
y1 being ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
x2,
y2 being ( ( ) (
complex V34()
ext-real )
Real) st
x1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= x2 : ( ( ) (
complex V34()
ext-real )
Real) &
y1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= y2 : ( ( ) (
complex V34()
ext-real )
Real) holds
addcomplex : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V25(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued V145(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V146(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) )
Element of
bool [:[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) ( complex-valued ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) : ( ( ) ( )
set ) )
. (
x1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ,
y1 : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= addreal : ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V25(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued V145(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V146(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) )
Element of
bool [:[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. (
x2 : ( ( ) (
complex V34()
ext-real )
Real) ,
y2 : ( ( ) (
complex V34()
ext-real )
Real) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ;
theorem
for
C being ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
G being ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
for
x1,
y1 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
x2,
y2 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) st
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
len x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
= len y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) & ( for
i being ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) st
i : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
in dom x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69() )
Element of
bool NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) holds
C : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
. (
(x1 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ,
(y1 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= G : ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
. (
(x2 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ,
(y2 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) holds
C : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
.: (
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ,
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= G : ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
.: (
x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ,
y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ;
theorem
for
x1,
y1 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
x2,
y2 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) st
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
len x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
= len y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) holds
addcomplex : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V25(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued V145(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V146(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) )
Element of
bool [:[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) ( complex-valued ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) : ( ( ) ( )
set ) )
.: (
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ,
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= addreal : ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V25(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued V145(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V146(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) )
Element of
bool [:[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
.: (
x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ,
y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ;
theorem
for
x1,
y1 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
x2,
y2 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) st
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) &
len x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
= len y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) holds
diffcomplex : ( (
Function-like V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like [:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V14(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) )
V18(
[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Element of
bool [:[:COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) ( complex-valued ) set ) ,COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) :] : ( ( ) (
complex-valued )
set ) : ( ( ) ( )
set ) )
.: (
x1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ,
y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= diffreal : ( (
Function-like V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like [:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V14(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) )
V18(
[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Element of
bool [:[:REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ,REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) :] : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
.: (
x2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ,
y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ;
theorem
for
h being ( (
Function-like V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like non
zero V14(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
g being ( (
Function-like V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like non
zero V14(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
for
y1 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
for
y2 being ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) st
len y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
= len y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) & ( for
i being ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) ) st
i : ( ( ) (
natural complex V34()
V35()
V36()
ext-real V64()
V65()
V66()
V67()
V68()
V69() )
Element of
NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) )
in dom y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69() )
Element of
bool NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) holds
h : ( (
Function-like V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like non
zero V14(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
. (y1 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ) FinSequence of COMPLEX : ( ( ) ( non zero V39() V64() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= g : ( (
Function-like V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like non
zero V14(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
. (y2 : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) -valued Function-like V39() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) ) . i : ( ( ) ( natural complex V34() V35() V36() ext-real V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V39() V64() V65() V66() V70() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
complex V34()
ext-real )
Element of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) holds
h : ( (
Function-like V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) ) (
Relation-like COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like non
zero V14(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
V18(
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
complex-valued )
Function of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ,
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
* y1 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued )
FinSequence of
COMPLEX : ( ( ) ( non
zero V39()
V64()
V70() )
set ) )
= g : ( (
Function-like V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ) (
Relation-like REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like non
zero V14(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
V18(
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ,
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) )
* y2 : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) : ( ( ) (
Relation-like NAT : ( ( ) (
V64()
V65()
V66()
V67()
V68()
V69()
V70() )
Element of
bool REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set )
-valued Function-like V39()
FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of
REAL : ( ( ) ( non
zero V39()
V64()
V65()
V66()
V70() )
set ) ) ;
begin