begin
definition
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ;
let h be ( (
real ) (
V11()
real ext-real )
number ) ;
func Shift (
f,
h)
-> ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
means
(
dom it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty V57()
V58()
V59()
V60()
V61()
V62() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) )
= (- h : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ) : ( (
V11() ) (
V11() )
set )
++ (dom f : ( ( non empty ) ( non empty ) set ) ) : ( ( ) (
V57()
V58()
V59() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) : ( ( ) (
V57()
V58()
V59() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in (- h : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ) : ( (
V11() ) (
V11() )
set )
++ (dom f : ( ( non empty ) ( non empty ) set ) ) : ( ( ) (
V57()
V58()
V59() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) : ( ( ) (
V57()
V58()
V59() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) holds
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= f : ( ( non
empty ) ( non
empty )
set )
. (x : ( ( ) ( V11() real ext-real ) Real) + h : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ) );
end;
definition
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ;
let h be ( (
real ) (
V11()
real ext-real )
number ) ;
func forward_difference (
f,
h)
-> ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Functional_Sequence of ( ( ) ( non
empty functional )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
means
(
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real V13()
non-empty empty-yielding V17(
RAT : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V60()
V63() )
set ) )
V30()
ext-real complex-valued ext-real-valued real-valued natural-valued V56()
V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= f : ( ( ) ( )
set ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real )
Nat) holds
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= fD (
(it : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) ) ,
h : ( ( ) ( )
set ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ) );
end;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= r : ( ( ) (
V11()
real ext-real )
Real)
* (((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) + f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((fdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (((fdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) - f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((fdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- (((fdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r1,
r2,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (((r1 : ( ( ) ( V11() real ext-real ) Real) (#) f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( V11() real ext-real ) Real) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (r1 : ( ( ) ( V11() real ext-real ) Real) * (((fdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (r2 : ( ( ) ( V11() real ext-real ) Real) * (((fdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((Shift (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
definition
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ;
let h be ( (
real ) (
V11()
real ext-real )
number ) ;
func backward_difference (
f,
h)
-> ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Functional_Sequence of ( ( ) ( non
empty functional )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
means
(
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real V13()
non-empty empty-yielding V17(
RAT : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V60()
V63() )
set ) )
V30()
ext-real complex-valued ext-real-valued real-valued natural-valued V56()
V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= f : ( ( ) ( )
set ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real )
Nat) holds
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= bD (
(it : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) ) ,
h : ( ( ) ( )
set ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ) );
end;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((bdif ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= r : ( ( ) (
V11()
real ext-real )
Real)
* (((bdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((bdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) + f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((bdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (((bdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((bdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) - f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((bdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- (((bdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r1,
r2,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((bdif (((r1 : ( ( ) ( V11() real ext-real ) Real) (#) f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( V11() real ext-real ) Real) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (r1 : ( ( ) ( V11() real ext-real ) Real) * (((bdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (r2 : ( ( ) ( V11() real ext-real ) Real) * (((bdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((bdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- ((Shift (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,(- h : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
definition
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ;
let h be ( (
real ) (
V11()
real ext-real )
number ) ;
func central_difference (
f,
h)
-> ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Functional_Sequence of ( ( ) ( non
empty functional )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
means
(
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real V13()
non-empty empty-yielding V17(
RAT : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V60()
V63() )
set ) )
V30()
ext-real complex-valued ext-real-valued real-valued natural-valued V56()
V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= f : ( ( ) ( )
set ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real )
Nat) holds
it : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
f : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) (
V13() )
set ) : ( ( ) ( )
set ) )
. (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
= cD (
(it : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) Nat) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) ) ,
h : ( ( ) ( )
set ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) ) );
end;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((cdif ((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= r : ( ( ) (
V11()
real ext-real )
Real)
* (((cdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((cdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) + f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((cdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (((cdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((cdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) - f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (((cdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- (((cdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
r1,
r2,
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((cdif (((r1 : ( ( ) ( V11() real ext-real ) Real) (#) f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( V11() real ext-real ) Real) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= (r1 : ( ( ) ( V11() real ext-real ) Real) * (((cdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (r2 : ( ( ) ( V11() real ext-real ) Real) * (((cdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((cdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((Shift (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,(h : ( ( ) ( V11() real ext-real ) Real) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
- ((Shift (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,(- (h : ( ( ) ( V11() real ext-real ) Real) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((bdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. (x : ( ( ) ( V11() real ext-real ) Real) + (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * h : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((cdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. (x : ( ( ) ( V11() real ext-real ) Real) + (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * h : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((cdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. ((x : ( ( ) ( V11() real ext-real ) Real) + (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * h : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) + (h : ( ( ) ( V11() real ext-real ) Real) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
definition
let f be ( (
V13()
Function-like real-valued ) (
V13()
Function-like complex-valued ext-real-valued real-valued )
Function) ;
let x0,
x1,
x2 be ( (
real ) (
V11()
real ext-real )
number ) ;
func [!f,x0,x1,x2!] -> ( ( ) (
V11()
real ext-real )
Real)
equals
([!f : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,x1 : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) !] : ( ( ) ( V11() real ext-real ) Real) - [!f : ( ( ) ( ) set ) ,x1 : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ,x2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) set ) !] : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
/ (x0 : ( ( ) ( ) set ) - x2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) set ) ) : ( ( ) ( )
set ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
end;
definition
let f be ( (
V13()
Function-like real-valued ) (
V13()
Function-like complex-valued ext-real-valued real-valued )
Function) ;
let x0,
x1,
x2,
x3 be ( (
real ) (
V11()
real ext-real )
number ) ;
func [!f,x0,x1,x2,x3!] -> ( ( ) (
V11()
real ext-real )
Real)
equals
([!f : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) ,x1 : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ,x2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) set ) !] : ( ( ) ( V11() real ext-real ) Real) - [!f : ( ( ) ( ) set ) ,x1 : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,(PFuncs (f : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) )) : ( ( ) ( non empty functional ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ,x2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) set ) ,x3 : ( ( ) ( V13() V16(f : ( ( ) ( ) set ) ) V17(x0 : ( ( ) ( ) set ) ) ) Element of bool [:f : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) !] : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
/ (x0 : ( ( ) ( ) set ) - x3 : ( ( ) ( V13() V16(f : ( ( ) ( ) set ) ) V17(x0 : ( ( ) ( ) set ) ) ) Element of bool [:f : ( ( ) ( ) set ) ,x0 : ( ( ) ( ) set ) :] : ( ( ) ( V13() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
set ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
end;
theorem
for
r,
x0,
x1 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
[!(r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= r : ( ( ) (
V11()
real ext-real )
Real)
* [!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
x0,
x1 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
[!(f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) + f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= [!f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
+ [!f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
r1,
r2,
x0,
x1 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
[!((r1 : ( ( ) ( V11() real ext-real ) Real) (#) f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (r2 : ( ( ) ( V11() real ext-real ) Real) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= (r1 : ( ( ) ( V11() real ext-real ) Real) * [!f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
+ (r2 : ( ( ) ( V11() real ext-real ) Real) * [!f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
x0,
x1,
x2 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) st
x0 : ( ( ) (
V11()
real ext-real )
Real) ,
x1 : ( ( ) (
V11()
real ext-real )
Real) ,
x2 : ( ( ) (
V11()
real ext-real )
Real)
are_mutually_different holds
(
[!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= [!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) ,x0 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) &
[!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= [!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x2 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x0 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
x0,
x1,
x2 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) st
x0 : ( ( ) (
V11()
real ext-real )
Real) ,
x1 : ( ( ) (
V11()
real ext-real )
Real) ,
x2 : ( ( ) (
V11()
real ext-real )
Real)
are_mutually_different holds
(
[!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= [!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x2 : ( ( ) ( V11() real ext-real ) Real) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) &
[!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real)
= [!f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,x1 : ( ( ) ( V11() real ext-real ) Real) ,x0 : ( ( ) ( V11() real ext-real ) Real) ,x2 : ( ( ) ( V11() real ext-real ) Real) !] : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
m,
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) holds
((fdif (((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((fdif (f : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) + n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ;
theorem
for
h,
x being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like quasi_total ) ( non
empty V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Function of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
for
S being ( (
Function-like quasi_total Sequence-yielding ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
PFuncs (
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ,
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) ( non
empty functional )
set ) )
Function-like total quasi_total Sequence-yielding )
Seq_Sequence) st ( for
n,
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) st
i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
<= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) holds
(S : ( ( Function-like quasi_total Sequence-yielding ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total Sequence-yielding ) Seq_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence)
. i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) choose i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * (((fdif (f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
* (((fdif (f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) -' i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( V11() real ext-real ) Real) + (i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) * h : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ) holds
(
((fdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= Sum (
(S : ( ( Function-like quasi_total Sequence-yielding ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total Sequence-yielding ) Seq_Sequence) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) ,1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real positive V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) &
((fdif ((f1 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) (#) f2 : ( ( Function-like quasi_total ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) ) : ( ( Function-like ) ( non empty V13() V16( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) V17( REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V13() complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ,h : ( ( ) ( V11() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total ) Functional_Sequence of ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) . 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) :] : ( ( ) (
V13()
complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
= Sum (
(S : ( ( Function-like quasi_total Sequence-yielding ) ( non empty V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V17( PFuncs (REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) ) : ( ( ) ( non empty functional ) set ) ) Function-like total quasi_total Sequence-yielding ) Seq_Sequence) . 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V32() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
Function-like quasi_total ) ( non
empty V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) )
V17(
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) ,2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real V30()
ext-real positive V56()
V57()
V58()
V59()
V60()
V61()
V62() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V57()
V58()
V59()
V60()
V61()
V62()
V63() )
Element of
bool REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V32()
V57()
V58()
V59()
V63() )
set ) ) ) ;