:: NDIFF_3 semantic presentation

REAL is V1() V34() V153() V154() V155() V159() set

NAT is V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() Element of K6(REAL)

K6(REAL) is V1() set

K332(REAL) is M10( REAL )

K7(NAT,K332(REAL)) is V13() set

K6(K7(NAT,K332(REAL))) is V1() set

K7(REAL,REAL) is V1() V13() complex-valued ext-real-valued real-valued set

K6(K7(REAL,REAL)) is V1() set

omega is V1() epsilon-transitive epsilon-connected ordinal V153() V154() V155() V156() V157() V158() V159() set

K6(omega) is V1() set

K6(NAT) is V1() set

K7(NAT,REAL) is V1() V13() complex-valued ext-real-valued real-valued set

K6(K7(NAT,REAL)) is V1() set

COMPLEX is V1() V34() V153() V159() set

RAT is V1() V34() V153() V154() V155() V156() V159() set

INT is V1() V34() V153() V154() V155() V156() V157() V159() set

K7(COMPLEX,COMPLEX) is V1() V13() complex-valued set

K6(K7(COMPLEX,COMPLEX)) is V1() set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is V1() V13() complex-valued set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V1() set

K7(K7(REAL,REAL),REAL) is V1() V13() complex-valued ext-real-valued real-valued set

K6(K7(K7(REAL,REAL),REAL)) is V1() set

K7(RAT,RAT) is V1() V13() V17( RAT ) complex-valued ext-real-valued real-valued set

K6(K7(RAT,RAT)) is V1() set

K7(K7(RAT,RAT),RAT) is V1() V13() V17( RAT ) complex-valued ext-real-valued real-valued set

K6(K7(K7(RAT,RAT),RAT)) is V1() set

K7(INT,INT) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued set

K6(K7(INT,INT)) is V1() set

K7(K7(INT,INT),INT) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued set

K6(K7(K7(INT,INT),INT)) is V1() set

K7(NAT,NAT) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued natural-valued set

K7(K7(NAT,NAT),NAT) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued natural-valued set

K6(K7(K7(NAT,NAT),NAT)) is V1() set

1 is 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

K7(1,1) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued natural-valued set

K6(K7(1,1)) is V1() set

K7(K7(1,1),1) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued natural-valued set

K6(K7(K7(1,1),1)) is V1() set

K7(K7(1,1),REAL) is V1() V13() complex-valued ext-real-valued real-valued set

K6(K7(K7(1,1),REAL)) is V1() set

2 is 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

K7(2,2) is V1() V13() V17( RAT ) V17( INT ) complex-valued ext-real-valued real-valued natural-valued set

K7(K7(2,2),REAL) is V1() V13() complex-valued ext-real-valued real-valued set

K6(K7(K7(2,2),REAL)) is V1() set

K461(2) is V195() L19()

the carrier of K461(2) is set

ExtREAL is V1() V154() set

0 is set

the V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V153() V154() V155() V156() V157() V158() V159() set is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V153() V154() V155() V156() V157() V158() V159() set

0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

NAT --> 0 is V1() T-Sequence-like V13() V16( NAT ) V17( NAT ) V17( RAT ) V17( INT ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))

K6(K7(NAT,NAT)) is V1() set

F is non empty V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() set

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

0. F is V53(F) Element of the carrier of F

Z is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

lim Z is V11() real ext-real Element of REAL

f is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim f is Element of the carrier of F

x is V11() real ext-real set

R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

L is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

Z . L is V11() real ext-real Element of REAL

(Z . L) - 0 is V11() real ext-real Element of REAL

abs ((Z . L) - 0) is V11() real ext-real Element of REAL

f . L is Element of the carrier of F

(f . L) - (0. F) is Element of the carrier of F

||.((f . L) - (0. F)).|| is V11() real ext-real non negative Element of REAL

||.(f . L).|| is V11() real ext-real non negative Element of REAL

abs (Z . L) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

F is non empty V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() set

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

Z is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

f is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

f ^\ Z is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of f

x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

x ^\ Z is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of x

(f ^\ Z) (#) (x ^\ Z) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f (#) x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(f (#) x) ^\ Z is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of f (#) x

R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

((f (#) x) ^\ Z) . R is Element of the carrier of F

R + Z is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

(f (#) x) . (R + Z) is Element of the carrier of F

x . (R + Z) is Element of the carrier of F

f . (R + Z) is V11() real ext-real Element of REAL

(f . (R + Z)) * (x . (R + Z)) is Element of the carrier of F

(f ^\ Z) . R is V11() real ext-real Element of REAL

((f ^\ Z) . R) * (x . (R + Z)) is Element of the carrier of F

(x ^\ Z) . R is Element of the carrier of F

((f ^\ Z) . R) * ((x ^\ Z) . R) is Element of the carrier of F

((f ^\ Z) (#) (x ^\ Z)) . R is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

0. F is V53(F) Element of the carrier of F

REAL --> (0. F) is V1() V13() V16( REAL ) V17( the carrier of F) Function-like constant total quasi_total Element of K6(K7(REAL, the carrier of F))

Z is V1() V13() V16( REAL ) V17( the carrier of F) Function-like constant total quasi_total Element of K6(K7(REAL, the carrier of F))

dom Z is V1() V153() V154() V155() Element of K6(REAL)

f is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

rng f is V1() V153() V154() V155() Element of K6(REAL)

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

Z /* f is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

f " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(f ") (#) (Z /* f) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((f ") (#) (Z /* f)) . x is Element of the carrier of F

(Z /* f) . x is Element of the carrier of F

(f ") . x is V11() real ext-real Element of REAL

((f ") . x) * ((Z /* f) . x) is Element of the carrier of F

f . x is V11() real ext-real Element of REAL

Z . (f . x) is Element of the carrier of F

((f ") . x) * (Z . (f . x)) is Element of the carrier of F

((f ") (#) (Z /* f)) . 0 is Element of the carrier of F

lim ((f ") (#) (Z /* f)) is Element of the carrier of F

f is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

Z /* f is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(f ") (#) (Z /* f) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

x is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

Z /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

x " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(x ") (#) (Z /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim ((x ") (#) (Z /* x)) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

0. F is V53(F) Element of the carrier of F

Z is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(REAL, the carrier of F))

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

f is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

Z + f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

Z - f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is Element of the carrier of F

R is Element of the carrier of F

dom (Z + f) is V153() V154() V155() Element of K6(REAL)

L is V11() real ext-real Element of REAL

(Z + f) . L is set

(Z + f) /. L is Element of the carrier of F

Z /. L is Element of the carrier of F

Z . L is Element of the carrier of F

f /. L is Element of the carrier of F

f . L is Element of the carrier of F

(Z /. L) + (f /. L) is Element of the carrier of F

L * x is Element of the carrier of F

(L * x) + (f . L) is Element of the carrier of F

L * R is Element of the carrier of F

(L * x) + (L * R) is Element of the carrier of F

x + R is Element of the carrier of F

L * (x + R) is Element of the carrier of F

dom (Z - f) is V153() V154() V155() Element of K6(REAL)

L is V11() real ext-real Element of REAL

(Z - f) . L is set

(Z - f) /. L is Element of the carrier of F

Z /. L is Element of the carrier of F

Z . L is Element of the carrier of F

f /. L is Element of the carrier of F

f . L is Element of the carrier of F

(Z /. L) - (f /. L) is Element of the carrier of F

L * x is Element of the carrier of F

(L * x) - (f . L) is Element of the carrier of F

L * R is Element of the carrier of F

(L * x) - (L * R) is Element of the carrier of F

x - R is Element of the carrier of F

L * (x - R) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V11() real ext-real Element of REAL

f is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

Z (#) f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is Element of the carrier of F

dom (Z (#) f) is V153() V154() V155() Element of K6(REAL)

R is V11() real ext-real Element of REAL

(Z (#) f) . R is set

(Z (#) f) /. R is Element of the carrier of F

f /. R is Element of the carrier of F

f . R is Element of the carrier of F

Z * (f /. R) is Element of the carrier of F

R * x is Element of the carrier of F

Z * (R * x) is Element of the carrier of F

Z * R is V11() real ext-real Element of REAL

(Z * R) * x is Element of the carrier of F

Z * x is Element of the carrier of F

R * (Z * x) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom Z is V153() V154() V155() Element of K6(REAL)

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom f is V153() V154() V155() Element of K6(REAL)

(dom Z) /\ (dom f) is V153() V154() V155() Element of K6(REAL)

Z + f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

Z - f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

rng x is V1() V153() V154() V155() Element of K6(REAL)

(Z + f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

Z /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) + (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z - f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) - (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

dom (Z + f) is V153() V154() V155() Element of K6(REAL)

R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

x . R is V11() real ext-real Element of REAL

((Z + f) /* x) . R is Element of the carrier of F

(Z + f) /. (x . R) is Element of the carrier of F

Z /. (x . R) is Element of the carrier of F

f /. (x . R) is Element of the carrier of F

(Z /. (x . R)) + (f /. (x . R)) is Element of the carrier of F

(Z /* x) . R is Element of the carrier of F

((Z /* x) . R) + (f /. (x . R)) is Element of the carrier of F

(f /* x) . R is Element of the carrier of F

((Z /* x) . R) + ((f /* x) . R) is Element of the carrier of F

dom (Z - f) is V153() V154() V155() Element of K6(REAL)

R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

x . R is V11() real ext-real Element of REAL

((Z - f) /* x) . R is Element of the carrier of F

(Z - f) /. (x . R) is Element of the carrier of F

Z /. (x . R) is Element of the carrier of F

f /. (x . R) is Element of the carrier of F

(Z /. (x . R)) - (f /. (x . R)) is Element of the carrier of F

(Z /* x) . R is Element of the carrier of F

((Z /* x) . R) - (f /. (x . R)) is Element of the carrier of F

(f /* x) . R is Element of the carrier of F

((Z /* x) . R) - ((f /* x) . R) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

Z + f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

Z - f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(Z + f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

Z /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) + (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z - f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) - (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

dom (Z + f) is V153() V154() V155() Element of K6(REAL)

dom Z is V153() V154() V155() Element of K6(REAL)

dom f is V153() V154() V155() Element of K6(REAL)

(dom Z) /\ (dom f) is V153() V154() V155() Element of K6(REAL)

rng x is V1() V153() V154() V155() Element of K6(REAL)

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

f is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

Z + f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

Z - f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

(Z + f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

x " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(x ") (#) ((Z + f) /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

Z /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) + (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) ((Z /* x) + (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (Z /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((x ") (#) (Z /* x)) + ((x ") (#) (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim ((x ") (#) (Z /* x)) is Element of the carrier of F

0. F is V53(F) Element of the carrier of F

lim ((x ") (#) (f /* x)) is Element of the carrier of F

lim ((x ") (#) ((Z + f) /* x)) is Element of the carrier of F

(0. F) + (0. F) is Element of the carrier of F

x is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

(Z - f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

x " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(x ") (#) ((Z - f) /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

Z /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* x) - (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) ((Z /* x) - (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (Z /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((x ") (#) (Z /* x)) - ((x ") (#) (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim ((x ") (#) (Z /* x)) is Element of the carrier of F

lim ((x ") (#) (f /* x)) is Element of the carrier of F

lim ((x ") (#) ((Z - f) /* x)) is Element of the carrier of F

(0. F) - (0. F) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V11() real ext-real Element of REAL

f is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

Z (#) f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom f is V153() V154() V155() Element of K6(REAL)

x is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

rng x is V1() V153() V154() V155() Element of K6(REAL)

(Z (#) f) /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

x " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(x ") (#) ((Z (#) f) /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

f /* x is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

Z * (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (Z * (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(x ") (#) (f /* x) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

Z * ((x ") (#) (f /* x)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim ((x ") (#) (f /* x)) is Element of the carrier of F

0. F is V53(F) Element of the carrier of F

lim ((x ") (#) ((Z (#) f) /* x)) is Element of the carrier of F

Z * (0. F) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

f is V11() real ext-real set

dom Z is V153() V154() V155() Element of K6(REAL)

Z /. f is Element of the carrier of F

x is V153() V154() V155() open Neighbourhood of f

R is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

R is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is Element of the carrier of F

R . 1 is Element of the carrier of F

1 * L is Element of the carrier of F

x is Element of the carrier of F

R is Element of the carrier of F

L is V153() V154() V155() open Neighbourhood of f

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

r is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is V153() V154() V155() open Neighbourhood of f

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

r is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

r is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

x0 is Element of the carrier of F

N is V153() V154() V155() open Neighbourhood of f

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

N is V153() V154() V155() open Neighbourhood of f

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L . 1 is Element of the carrier of F

R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

p is Element of the carrier of F

s1 is V153() V154() V155() open Neighbourhood of f

h is V11() real ext-real set

f - h is V11() real ext-real Element of REAL

f + h is V11() real ext-real Element of REAL

].(f - h),(f + h).[ is V153() V154() V155() open Element of K6(REAL)

{ b

M is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

z0 + 2 is 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

h / (z0 + 2) is V11() real ext-real Element of REAL

M . z0 is V11() real ext-real Element of REAL

lim M is V11() real ext-real Element of REAL

z0 is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

z0 . z0 is V11() real ext-real Element of REAL

z0 + 2 is 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

h / (z0 + 2) is V11() real ext-real Element of REAL

f + (h / (z0 + 2)) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

x - f is V11() real ext-real Element of REAL

z0 + 1 is 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

(z0 + 1) + 1 is 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

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

z0 + 1 is 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

h / 1 is V11() real ext-real Element of REAL

- h is V11() real ext-real Element of REAL

f + (- h) is V11() real ext-real Element of REAL

1 * p is Element of the carrier of F

1 * x0 is Element of the carrier of F

z0 is V11() real ext-real Element of REAL

Z /. z0 is Element of the carrier of F

(Z /. z0) - (Z /. f) is Element of the carrier of F

z0 - f is V11() real ext-real Element of REAL

L . (z0 - f) is Element of the carrier of F

r /. (z0 - f) is Element of the carrier of F

(L . (z0 - f)) + (r /. (z0 - f)) is Element of the carrier of F

L . (z0 - f) is Element of the carrier of F

R /. (z0 - f) is Element of the carrier of F

(L . (z0 - f)) + (R /. (z0 - f)) is Element of the carrier of F

(z0 - f) * x0 is Element of the carrier of F

((z0 - f) * x0) + (r /. (z0 - f)) is Element of the carrier of F

(z0 - f) * 1 is V11() real ext-real Element of REAL

((z0 - f) * 1) * x0 is Element of the carrier of F

(((z0 - f) * 1) * x0) + (r /. (z0 - f)) is Element of the carrier of F

((z0 - f) * 1) * p is Element of the carrier of F

(((z0 - f) * 1) * p) + (R /. (z0 - f)) is Element of the carrier of F

((z0 - f) * 1) * x is Element of the carrier of F

(((z0 - f) * 1) * x) + (r /. (z0 - f)) is Element of the carrier of F

(z0 - f) * x is Element of the carrier of F

((z0 - f) * x) + (r /. (z0 - f)) is Element of the carrier of F

(z0 - f) * R is Element of the carrier of F

((z0 - f) * R) + (R /. (z0 - f)) is Element of the carrier of F

dom R is V153() V154() V155() Element of K6(REAL)

rng z0 is V1() V153() V154() V155() Element of K6(REAL)

dom r is V153() V154() V155() Element of K6(REAL)

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

z0 . z0 is V11() real ext-real Element of REAL

(z0 . z0) * x is Element of the carrier of F

r /. (z0 . z0) is Element of the carrier of F

((z0 . z0) * x) + (r /. (z0 . z0)) is Element of the carrier of F

(z0 . z0) * R is Element of the carrier of F

R /. (z0 . z0) is Element of the carrier of F

((z0 . z0) * R) + (R /. (z0 . z0)) is Element of the carrier of F

x is V11() real ext-real Element of REAL

x - f is V11() real ext-real Element of REAL

1 / (z0 . z0) is V11() real ext-real Element of REAL

(1 / (z0 . z0)) * ((z0 . z0) * x) is Element of the carrier of F

(1 / (z0 . z0)) * (r /. (z0 . z0)) is Element of the carrier of F

((1 / (z0 . z0)) * ((z0 . z0) * x)) + ((1 / (z0 . z0)) * (r /. (z0 . z0))) is Element of the carrier of F

(1 / (z0 . z0)) * (((z0 . z0) * R) + (R /. (z0 . z0))) is Element of the carrier of F

(1 / (z0 . z0)) * (z0 . z0) is V11() real ext-real Element of REAL

((1 / (z0 . z0)) * (z0 . z0)) * x is Element of the carrier of F

(((1 / (z0 . z0)) * (z0 . z0)) * x) + ((1 / (z0 . z0)) * (r /. (z0 . z0))) is Element of the carrier of F

(1 / (z0 . z0)) * ((z0 . z0) * R) is Element of the carrier of F

(1 / (z0 . z0)) * (R /. (z0 . z0)) is Element of the carrier of F

((1 / (z0 . z0)) * ((z0 . z0) * R)) + ((1 / (z0 . z0)) * (R /. (z0 . z0))) is Element of the carrier of F

(z0 . z0) " is V11() real ext-real Element of REAL

((z0 . z0) ") * (r /. (z0 . z0)) is Element of the carrier of F

z0 " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(z0 ") . z0 is V11() real ext-real Element of REAL

((z0 ") . z0) * (r /. (z0 . z0)) is Element of the carrier of F

r /* z0 is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

(r /* z0) . z0 is Element of the carrier of F

((z0 ") . z0) * ((r /* z0) . z0) is Element of the carrier of F

(z0 ") (#) (r /* z0) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((z0 ") (#) (r /* z0)) . z0 is Element of the carrier of F

((z0 . z0) ") * (R /. (z0 . z0)) is Element of the carrier of F

((z0 ") . z0) * (R /. (z0 . z0)) is Element of the carrier of F

R /* z0 is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(R /* z0) . z0 is Element of the carrier of F

((z0 ") . z0) * ((R /* z0) . z0) is Element of the carrier of F

(z0 ") (#) (R /* z0) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((z0 ") (#) (R /* z0)) . z0 is Element of the carrier of F

((1 / (z0 . z0)) * (z0 . z0)) * R is Element of the carrier of F

1 * R is Element of the carrier of F

1 * x is Element of the carrier of F

x + (((z0 ") (#) (r /* z0)) . z0) is Element of the carrier of F

R + (((z0 ") (#) (R /* z0)) . z0) is Element of the carrier of F

(((z0 ") (#) (r /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0) is Element of the carrier of F

x + ((((z0 ") (#) (r /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0)) is Element of the carrier of F

(R + (((z0 ") (#) (R /* z0)) . z0)) - (((z0 ") (#) (r /* z0)) . z0) is Element of the carrier of F

(((z0 ") (#) (R /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0) is Element of the carrier of F

R + ((((z0 ") (#) (R /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0)) is Element of the carrier of F

0. F is V53(F) Element of the carrier of F

x + (0. F) is Element of the carrier of F

x - R is Element of the carrier of F

R - R is Element of the carrier of F

((((z0 ") (#) (R /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0)) + (R - R) is Element of the carrier of F

((((z0 ") (#) (R /* z0)) . z0) - (((z0 ") (#) (r /* z0)) . z0)) + (0. F) is Element of the carrier of F

((z0 ") (#) (R /* z0)) - ((z0 ") (#) (r /* z0)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(((z0 ") (#) (R /* z0)) - ((z0 ") (#) (r /* z0))) . z0 is Element of the carrier of F

(((z0 ") (#) (R /* z0)) - ((z0 ") (#) (r /* z0))) . 0 is Element of the carrier of F

lim (((z0 ") (#) (R /* z0)) - ((z0 ") (#) (r /* z0))) is Element of the carrier of F

lim ((z0 ") (#) (R /* z0)) is Element of the carrier of F

lim ((z0 ") (#) (r /* z0)) is Element of the carrier of F

(0. F) - (0. F) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is set

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom f is V153() V154() V155() Element of K6(REAL)

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V153() V154() V155() open Element of K6(REAL)

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom f is V153() V154() V155() Element of K6(REAL)

x is V11() real ext-real Element of REAL

f | Z is V13() V16( REAL ) V16(Z) V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom (f | Z) is V153() V154() V155() Element of K6(Z)

K6(Z) is V1() set

(f | Z) /. x is Element of the carrier of F

R is V153() V154() V155() open Neighbourhood of x

f /. x is Element of the carrier of F

(dom f) /\ Z is V153() V154() V155() Element of K6(REAL)

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

L is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

r is V11() real ext-real Element of REAL

(f | Z) /. r is Element of the carrier of F

((f | Z) /. r) - ((f | Z) /. x) is Element of the carrier of F

r - x is V11() real ext-real Element of REAL

L . (r - x) is Element of the carrier of F

L /. (r - x) is Element of the carrier of F

(L . (r - x)) + (L /. (r - x)) is Element of the carrier of F

f /. r is Element of the carrier of F

(f /. r) - ((f | Z) /. x) is Element of the carrier of F

(f /. r) - (f /. x) is Element of the carrier of F

f | Z is V13() V16( REAL ) V16(Z) V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is V11() real ext-real Element of REAL

R is V153() V154() V155() open Neighbourhood of x

f /. x is Element of the carrier of F

L is V153() V154() V155() open Neighbourhood of x

L is V153() V154() V155() open Neighbourhood of x

dom (f | Z) is V153() V154() V155() Element of K6(REAL)

(f | Z) /. x is Element of the carrier of F

(dom f) /\ Z is V153() V154() V155() Element of K6(REAL)

dom (f | Z) is V153() V154() V155() Element of K6(Z)

K6(Z) is V1() set

r is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

x0 is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

r is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

x0 is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

N is V11() real ext-real Element of REAL

f /. N is Element of the carrier of F

(f /. N) - (f /. x) is Element of the carrier of F

N - x is V11() real ext-real Element of REAL

r . (N - x) is Element of the carrier of F

x0 /. (N - x) is Element of the carrier of F

(r . (N - x)) + (x0 /. (N - x)) is Element of the carrier of F

(f | Z) /. N is Element of the carrier of F

((f | Z) /. N) - (f /. x) is Element of the carrier of F

((f | Z) /. N) - ((f | Z) /. x) is Element of the carrier of F

N is V11() real ext-real Element of REAL

(f | Z) /. N is Element of the carrier of F

((f | Z) /. N) - ((f | Z) /. x) is Element of the carrier of F

N - x is V11() real ext-real Element of REAL

r . (N - x) is Element of the carrier of F

x0 /. (N - x) is Element of the carrier of F

(r . (N - x)) + (x0 /. (N - x)) is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V153() V154() V155() Element of K6(REAL)

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

x is V11() real ext-real set

f | Z is V13() V16( REAL ) V16(Z) V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom (f | Z) is V153() V154() V155() Element of K6(Z)

K6(Z) is V1() set

(f | Z) /. x is Element of the carrier of F

R is V153() V154() V155() open Neighbourhood of x

L is V153() V154() V155() open Neighbourhood of x

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

f is set

x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom x is V153() V154() V155() Element of K6(REAL)

R is set

R is set

R is V11() real ext-real Element of REAL

x . R is set

(F,Z,R) is Element of the carrier of F

R is V11() real ext-real Element of REAL

x . R is set

(F,Z,R) is Element of the carrier of F

x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom x is V153() V154() V155() Element of K6(REAL)

R is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom R is V153() V154() V155() Element of K6(REAL)

L is V11() real ext-real Element of REAL

x . L is set

(F,Z,L) is Element of the carrier of F

R . L is set

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

0. F is V53(F) Element of the carrier of F

Z is V153() V154() V155() open Element of K6(REAL)

f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom f is V153() V154() V155() Element of K6(REAL)

rng f is Element of K6( the carrier of F)

K6( the carrier of F) is V1() set

(F,f,Z) is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

REAL --> (0. F) is V1() V13() V16( REAL ) V17( the carrier of F) Function-like constant total quasi_total Element of K6(K7(REAL, the carrier of F))

dom (REAL --> (0. F)) is V1() V153() V154() V155() Element of K6(REAL)

R is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

rng R is V1() V153() V154() V155() Element of K6(REAL)

L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(REAL --> (0. F)) /* R is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

R " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R ") (#) ((REAL --> (0. F)) /* R) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((R ") (#) ((REAL --> (0. F)) /* R)) . L is Element of the carrier of F

((REAL --> (0. F)) /* R) . L is Element of the carrier of F

(R ") . L is V11() real ext-real Element of REAL

((R ") . L) * (((REAL --> (0. F)) /* R) . L) is Element of the carrier of F

R . L is V11() real ext-real Element of REAL

(REAL --> (0. F)) /. (R . L) is Element of the carrier of F

(REAL --> (0. F)) . (R . L) is Element of the carrier of F

((R ") . L) * ((REAL --> (0. F)) /. (R . L)) is Element of the carrier of F

((R ") (#) ((REAL --> (0. F)) /* R)) . 0 is Element of the carrier of F

lim ((R ") (#) ((REAL --> (0. F)) /* R)) is Element of the carrier of F

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(REAL, the carrier of F))

L is V11() real ext-real Element of REAL

L . L is Element of the carrier of F

L * (0. F) is Element of the carrier of F

r is Element of the carrier of F

{r} is set

x0 is V11() real ext-real Element of REAL

f /. x0 is Element of the carrier of F

f . x0 is set

x0 is V11() real ext-real Element of REAL

N is V153() V154() V155() open Neighbourhood of x0

f /. x0 is Element of the carrier of F

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

L is V11() real ext-real Element of REAL

f /. L is Element of the carrier of F

(f /. L) - (f /. x0) is Element of the carrier of F

L - x0 is V11() real ext-real Element of REAL

L . (L - x0) is Element of the carrier of F

R /. (L - x0) is Element of the carrier of F

(L . (L - x0)) + (R /. (L - x0)) is Element of the carrier of F

R . (L - x0) is set

r - (f /. x0) is Element of the carrier of F

r - r is Element of the carrier of F

x0 is V11() real ext-real Element of REAL

(F,f,Z) /. x0 is Element of the carrier of F

f /. x0 is Element of the carrier of F

N is V153() V154() V155() open Neighbourhood of x0

L is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

N is V153() V154() V155() open Neighbourhood of x0

L is V11() real ext-real Element of REAL

f /. L is Element of the carrier of F

(f /. L) - (f /. x0) is Element of the carrier of F

L - x0 is V11() real ext-real Element of REAL

L . (L - x0) is Element of the carrier of F

R /. (L - x0) is Element of the carrier of F

(L . (L - x0)) + (R /. (L - x0)) is Element of the carrier of F

R . (L - x0) is set

r - (f /. x0) is Element of the carrier of F

r - r is Element of the carrier of F

dom (F,f,Z) is V153() V154() V155() Element of K6(REAL)

(F,f,Z) . x0 is set

(F,f,x0) is Element of the carrier of F

L . 1 is Element of the carrier of F

F is non empty non trivial V72() V97() V98() V99() V100() V101() V102() V103() V107() V108() RealNormSpace-like NORMSTR

the carrier of F is V1() non trivial set

K7(REAL, the carrier of F) is V1() V13() set

K6(K7(REAL, the carrier of F)) is V1() set

Z is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))

dom Z is V153() V154() V155() Element of K6(REAL)

f is V11() real ext-real set

{f} is V153() V154() V155() set

(F,Z,f) is Element of the carrier of F

x is V153() V154() V155() open Neighbourhood of f

Z /. f is Element of the carrier of F

R is V153() V154() V155() open Neighbourhood of f

L is V153() V154() V155() open Neighbourhood of f

L is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

L " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

r is V1() V13() V16( NAT ) V17( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))

rng r is V1() V153() V154() V155() Element of K6(REAL)

L + r is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

rng (L + r) is V1() V153() V154() V155() Element of K6(REAL)

Z /* (L + r) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

K7(NAT, the carrier of F) is V1() V13() set

K6(K7(NAT, the carrier of F)) is V1() set

Z /* r is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(Z /* (L + r)) - (Z /* r) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(L ") (#) ((Z /* (L + r)) - (Z /* r)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim ((L ") (#) ((Z /* (L + r)) - (Z /* r))) is Element of the carrier of F

x0 is V11() real ext-real set

f - x0 is V11() real ext-real Element of REAL

f + x0 is V11() real ext-real Element of REAL

].(f - x0),(f + x0).[ is V153() V154() V155() open Element of K6(REAL)

{ b

N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

f + N is V11() real ext-real Element of REAL

f - 0 is V11() real ext-real Element of REAL

L is set

lim r is V11() real ext-real Element of REAL

lim L is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V153() V154() V155() V156() V157() V158() V159() Element of REAL

L is V11() real ext-real Element of REAL

lim (L + r) is V11() real ext-real Element of REAL

L + f is V11() real ext-real Element of REAL

R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

r ^\ R is V1() V13() V16( NAT ) V17( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of r

rng (r ^\ R) is V1() V153() V154() V155() Element of K6(REAL)

(L + r) ^\ R is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of L + r

rng ((L + r) ^\ R) is V1() V153() V154() V155() Element of K6(REAL)

p is set

p is set

s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

((L + r) ^\ R) . s1 is V11() real ext-real Element of REAL

h is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

R + h is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

R + s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

(L + r) . (R + s1) is V11() real ext-real Element of REAL

((L + r) . (R + s1)) - f is V11() real ext-real Element of REAL

abs (((L + r) . (R + s1)) - f) is V11() real ext-real Element of REAL

s1 + R is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

(L + r) . (s1 + R) is V11() real ext-real Element of REAL

((L + r) . (s1 + R)) - f is V11() real ext-real Element of REAL

(((L + r) ^\ R) . s1) - f is V11() real ext-real Element of REAL

- x0 is V11() real ext-real Element of REAL

f + (- x0) is V11() real ext-real Element of REAL

L is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

r ^\ L is V1() V13() V16( NAT ) V17( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of r

rng (r ^\ L) is V1() V153() V154() V155() Element of K6(REAL)

(L + r) ^\ L is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of L + r

rng ((L + r) ^\ L) is V1() V153() V154() V155() Element of K6(REAL)

L is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

r ^\ L is V1() V13() V16( NAT ) V17( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of r

rng (r ^\ L) is V1() V153() V154() V155() Element of K6(REAL)

(L + r) ^\ L is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of L + r

rng ((L + r) ^\ L) is V1() V153() V154() V155() Element of K6(REAL)

R is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

p is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

R is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total (F) Element of K6(K7(REAL, the carrier of F))

p is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))

s1 is set

L ^\ L is V1() V13() non-empty V16( NAT ) V17( REAL ) Function-like total quasi_total 0 -convergent complex-valued ext-real-valued real-valued convergent subsequence of L

R /* (L ^\ L) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

p /* (L ^\ L) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(R /* (L ^\ L)) + (p /* (L ^\ L)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(L ^\ L) " is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((L ^\ L) ") (#) ((R /* (L ^\ L)) + (p /* (L ^\ L))) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim (((L ^\ L) ") (#) ((R /* (L ^\ L)) + (p /* (L ^\ L)))) is Element of the carrier of F

R . 1 is Element of the carrier of F

((L ^\ L) ") (#) (p /* (L ^\ L)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

s1 is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

lim (((L ^\ L) ") (#) (p /* (L ^\ L))) is Element of the carrier of F

0. F is V53(F) Element of the carrier of F

h is V11() real ext-real Element of REAL

M is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

s1 . z0 is Element of the carrier of F

(s1 . z0) - (R . 1) is Element of the carrier of F

||.((s1 . z0) - (R . 1)).|| is V11() real ext-real non negative Element of REAL

(((L ^\ L) ") (#) (p /* (L ^\ L))) . z0 is Element of the carrier of F

(R . 1) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) is Element of the carrier of F

((R . 1) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0)) - (R . 1) is Element of the carrier of F

||.(((R . 1) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0)) - (R . 1)).|| is V11() real ext-real non negative Element of REAL

(R . 1) - (R . 1) is Element of the carrier of F

((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) + ((R . 1) - (R . 1)) is Element of the carrier of F

||.(((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) + ((R . 1) - (R . 1))).|| is V11() real ext-real non negative Element of REAL

((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) + (0. F) is Element of the carrier of F

||.(((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) + (0. F)).|| is V11() real ext-real non negative Element of REAL

||.((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0).|| is V11() real ext-real non negative Element of REAL

((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) - (0. F) is Element of the carrier of F

||.(((((L ^\ L) ") (#) (p /* (L ^\ L))) . z0) - (0. F)).|| is V11() real ext-real non negative Element of REAL

h is Element of the carrier of F

1 * h is Element of the carrier of F

M is epsilon-transitive epsilon-connected ordinal natural V11() real V112() ext-real non negative V152() V153() V154() V155() V156() V157() V158() Element of NAT

(L ^\ L) . M is V11() real ext-real Element of REAL

(((L ^\ L) ") (#) ((R /* (L ^\ L)) + (p /* (L ^\ L)))) . M is Element of the carrier of F

((L ^\ L) ") (#) (R /* (L ^\ L)) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

(((L ^\ L) ") (#) (R /* (L ^\ L))) + (((L ^\ L) ") (#) (p /* (L ^\ L))) is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))

((((L ^\ L) ") (#) (R /* (L ^\ L))) + (((L ^\ L) ") (#) (p /* (L ^\ L)))) . M is Element of the carrier of F

(((L ^\ L) ") (#) (R /* (L ^\ L))) . M is Element of the carrier of F

(((L ^\ L) ") (#) (p /* (L ^\ L))) . M is Element of the carrier of F

((((L ^\ L) ") (#) (R /* (L ^\ L))) . M) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F

(R /* (L ^\ L)) . M is Element of the carrier of F

((L ^\ L) ") . M is V11() real ext-real Element of REAL

(((L