begin
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
h1,
h2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
for
seq being ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) st
rng seq : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) : ( ( ) (
V1()
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) )
c= (dom h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) )
/\ (dom h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) holds
(
(h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) + h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
/* seq : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
= (h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
+ (h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) &
(h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) - h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
/* seq : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
= (h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
- (h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
h1,
h2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
for
seq being ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) st
h1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) is
total &
h2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) is
total holds
(
(h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) + h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
/* seq : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
= (h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
+ (h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) &
(h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) - h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
/* seq : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
= (h1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
- (h2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ) ;
definition
let F be ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) ;
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) ;
let x0 be ( (
real ) (
V11()
real ext-real )
number ) ;
pred f is_differentiable_in x0 means
ex
N being ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ) st
(
N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
real ) (
V11()
real ext-real )
number ) )
c= dom f : ( ( ) ( )
Element of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) & ex
L being ( (
Function-like quasi_total linear ) (
V1()
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total linear )
LinearFunc of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) ex
R being ( (
Function-like RestFunc-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like RestFunc-like )
RestFunc of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) st
for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
real ) (
V11()
real ext-real )
number ) ) holds
(f : ( ( ) ( ) Element of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) /. x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
- (f : ( ( ) ( ) Element of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) /. x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
= (L : ( ( Function-like quasi_total linear ) ( V1() V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total linear ) LinearFunc of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) ) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
+ (R : ( ( Function-like RestFunc-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like RestFunc-like ) RestFunc of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) ) /. (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) );
end;
definition
let F be ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) ;
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) ;
let x0 be ( (
real ) (
V11()
real ext-real )
number ) ;
assume
f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( (
real ) (
V11()
real ext-real )
number )
;
func diff (
f,
x0)
-> ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
means
ex
N being ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ) st
(
N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
real ) (
V11()
real ext-real )
number ) )
c= dom f : ( ( ) ( )
Element of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) & ex
L being ( (
Function-like quasi_total linear ) (
V1()
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total linear )
LinearFunc of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) ex
R being ( (
Function-like RestFunc-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like RestFunc-like )
RestFunc of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) st
(
it : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
= L : ( (
Function-like quasi_total linear ) (
V1()
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total linear )
LinearFunc of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) )
. 1 : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal natural V11()
real V112()
ext-real positive non
negative V152()
V153()
V154()
V155()
V156()
V157()
V158() )
Element of
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
real ) (
V11()
real ext-real )
number ) ) holds
(f : ( ( ) ( ) Element of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) /. x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
- (f : ( ( ) ( ) Element of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) /. x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
= (L : ( ( Function-like quasi_total linear ) ( V1() V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total linear ) LinearFunc of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) ) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
+ (R : ( ( Function-like RestFunc-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like RestFunc-like ) RestFunc of F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) ) /. (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( Function-like quasi_total ) ( V13() V16(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) V17(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) Function-like quasi_total ) Element of K6(K7(K7(F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ,F : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) NORMSTR ) ) : ( ( ) ( V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) ) ) );
end;
definition
let F be ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) ;
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) ;
let X be ( ( ) ( )
set ) ;
pred f is_differentiable_on X means
(
X : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
c= dom f : ( ( ) ( )
Element of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in X : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) holds
f : ( ( ) ( )
Element of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
| X : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_in x : ( ( ) (
V11()
real ext-real )
Real) ) );
end;
definition
let F be ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) ;
let f be ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) ;
let X be ( ( ) ( )
set ) ;
assume
f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on X : ( ( ) ( )
set )
;
func f `| X -> ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
means
(
dom it : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V13()
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) )
= X : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in X : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) holds
it : ( (
Function-like quasi_total ) (
V13()
V16(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) )
V17(
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ,
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) : ( ( ) (
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) ( )
set )
= diff (
f : ( ( ) ( )
Element of
F : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
NORMSTR ) ) ,
x : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) ) );
end;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
f being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
for
x0 being ( (
real ) (
V11()
real ext-real )
number )
for
N being ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
x0 : ( (
real ) (
V11()
real ext-real )
number ) ) st
f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( (
real ) (
V11()
real ext-real )
number ) &
N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
b3 : ( (
real ) (
V11()
real ext-real )
number ) )
c= dom f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) holds
for
h being ( (
non-zero Function-like quasi_total 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V112()
ext-real non
negative V152()
V153()
V154()
V155()
V156()
V157()
V158() )
Element of
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
-convergent ) (
V1()
V13()
non-zero V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V112()
ext-real non
negative V152()
V153()
V154()
V155()
V156()
V157()
V158() )
Element of
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
-convergent complex-valued ext-real-valued real-valued convergent )
Real_Sequence)
for
c being ( (
Function-like constant quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent )
Real_Sequence) st
rng c : ( (
Function-like constant quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent )
Real_Sequence) : ( ( ) (
V1()
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) )
= {x0 : ( ( real ) ( V11() real ext-real ) number ) } : ( ( ) (
V153()
V154()
V155() )
set ) &
rng (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent ) ( V1() V13() non-zero V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent complex-valued ext-real-valued real-valued convergent ) Real_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( (
Function-like ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) ,
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1()
V13()
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V1()
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) )
c= N : ( ( ) (
V153()
V154()
V155()
open )
Neighbourhood of
b3 : ( (
real ) (
V11()
real ext-real )
number ) ) holds
(
(h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent ) ( V1() V13() non-zero V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ") : ( (
Function-like ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
Function-like total quasi_total complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) ,
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1()
V13()
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) (
V1() )
set ) )
(#) ((f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent ) ( V1() V13() non-zero V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent complex-valued ext-real-valued real-valued convergent ) Real_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( Function-like ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ,REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() V13() complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) - (f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* c : ( ( Function-like constant quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) is
convergent &
diff (
f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) ,
x0 : ( (
real ) (
V11()
real ext-real )
number ) ) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
= lim ((h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent ) ( V1() V13() non-zero V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ") : ( ( Function-like ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ,REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() V13() complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( V1() ) set ) ) (#) ((f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent ) ( V1() V13() non-zero V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() ) Element of NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) -convergent complex-valued ext-real-valued real-valued convergent ) Real_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( Function-like ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ,REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() V13() complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) - (f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) /* c : ( ( Function-like constant quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( ( Function-like quasi_total ) ( V1() V13() V16( NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like total quasi_total ) Element of K6(K7(NAT : ( ( ) ( V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() ) Element of K6(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) : ( ( ) ( V1() ) set ) ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) ) : ( (
Function-like quasi_total ) (
V1()
V13()
V16(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
NAT : ( ( ) (
V1()
epsilon-transitive epsilon-connected ordinal V153()
V154()
V155()
V156()
V157()
V158()
V159() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) st
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) holds
(
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
+ f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
diff (
(f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
= (diff (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
+ (diff (f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) st
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) holds
(
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
- f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
diff (
(f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
= (diff (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
- (diff (f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
Z being ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
for
f1,
f2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) st
Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
c= dom (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) &
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) &
f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
(
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
+ f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
((f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) Element of K6(K7(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) `| Z : ( ( open ) ( V153() V154() V155() open ) Subset of ( ( ) ( V1() ) set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) ( )
set )
= (diff (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
+ (diff (f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
Z being ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
for
f1,
f2 being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) st
Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
c= dom (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) &
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) &
f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
(
f1 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
- f2 : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
((f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) Element of K6(K7(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) `| Z : ( ( open ) ( V153() V154() V155() open ) Subset of ( ( ) ( V1() ) set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) ( )
set )
= (diff (f1 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) )
- (diff (f2 : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ) ;
theorem
for
F being ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace)
for
r being ( ( ) (
V11()
real ext-real )
Real)
for
Z being ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
for
f being ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) st
Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) )
c= dom (r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) ) : ( ( ) (
V153()
V154()
V155() )
Element of
K6(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) ) : ( ( ) (
V1() )
set ) ) &
f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
(
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
Element of
K6(
K7(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) , the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) (
V1()
V13() )
set ) ) : ( ( ) (
V1() )
set ) )
is_differentiable_on Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) & ( for
x being ( ( ) (
V11()
real ext-real )
Real) st
x : ( ( ) (
V11()
real ext-real )
Real)
in Z : ( (
open ) (
V153()
V154()
V155()
open )
Subset of ( ( ) (
V1() )
set ) ) holds
((r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) Element of K6(K7(REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) , the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) : ( ( ) ( V1() V13() ) set ) ) : ( ( ) ( V1() ) set ) ) `| Z : ( ( open ) ( V153() V154() V155() open ) Subset of ( ( ) ( V1() ) set ) ) ) : ( (
Function-like ) (
V13()
V16(
REAL : ( ( ) (
V1()
V34()
V153()
V154()
V155()
V159() )
set ) )
V17( the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) )
Function-like )
PartFunc of ,)
. x : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) ( )
set )
= r : ( ( ) (
V11()
real ext-real )
Real)
* (diff (f : ( ( Function-like ) ( V13() V16( REAL : ( ( ) ( V1() V34() V153() V154() V155() V159() ) set ) ) V17( the carrier of b1 : ( ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) ( non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like ) RealNormSpace) : ( ( ) ( V1() non trivial ) set ) ) Function-like ) PartFunc of ,) ,x : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( )
Point of ( ( ) (
V1() non
trivial )
set ) ) : ( ( ) ( )
Element of the
carrier of
b1 : ( ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like ) ( non
empty non
trivial V72()
V97()
V98()
V99()
V100()
V101()
V102()
V103()
V107()
V108()
RealNormSpace-like )
RealNormSpace) : ( ( ) (
V1() non
trivial )
set ) ) ) ) ;