:: 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₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - h & not f + h <= b₁ ) } is set
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₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - x0 & not f + x0 <= b₁ ) } is set
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 ^\ L) ") . M) * ((R /* (L ^\ L)) . M) is Element of the carrier of F
((((L ^\ L) ") . M) * ((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) * (R . ((L ^\ L) . M)) is Element of the carrier of F
((((L ^\ L) ") . M) * (R . ((L ^\ L) . M))) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
((L ^\ L) . M) * h is Element of the carrier of F
(((L ^\ L) ") . M) * (((L ^\ L) . M) * h) is Element of the carrier of F
((((L ^\ L) ") . M) * (((L ^\ L) . M) * h)) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
((L ^\ L) . M) " is V11() real ext-real Element of REAL
(((L ^\ L) . M) ") * (((L ^\ L) . M) * h) is Element of the carrier of F
((((L ^\ L) . M) ") * (((L ^\ L) . M) * h)) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
(((L ^\ L) . M) ") * ((L ^\ L) . M) is V11() real ext-real Element of REAL
((((L ^\ L) . M) ") * ((L ^\ L) . M)) * h is Element of the carrier of F
(((((L ^\ L) . M) ") * ((L ^\ L) . M)) * h) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
(1 * h) + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
h + ((((L ^\ L) ") (#) (p /* (L ^\ L))) . M) is Element of the carrier of F
s1 . M is Element of the carrier of F
s1 is set
s1 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) ^\ L) . s1 is V11() real ext-real Element of REAL
Z /. (((L + r) ^\ L) . s1) is Element of the carrier of F
(r ^\ L) . s1 is V11() real ext-real Element of REAL
Z /. ((r ^\ L) . s1) is Element of the carrier of F
(Z /. (((L + r) ^\ L) . s1)) - (Z /. ((r ^\ L) . s1)) is Element of the carrier of F
(L ^\ L) . s1 is V11() real ext-real Element of REAL
R . ((L ^\ L) . s1) is Element of the carrier of F
p /. ((L ^\ L) . s1) is Element of the carrier of F
(R . ((L ^\ L) . s1)) + (p /. ((L ^\ L) . s1)) is Element of the carrier of F
(((L + r) ^\ L) . s1) - ((r ^\ L) . s1) is V11() real ext-real Element of REAL
(L ^\ L) + (r ^\ 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)) . s1 is V11() real ext-real Element of REAL
(((L ^\ L) + (r ^\ L)) . s1) - ((r ^\ L) . s1) is V11() real ext-real Element of REAL
((L ^\ L) . s1) + ((r ^\ L) . s1) is V11() real ext-real Element of REAL
(((L ^\ L) . s1) + ((r ^\ L) . s1)) - ((r ^\ L) . s1) is V11() real ext-real Element of REAL
dom p is V153() V154() V155() Element of K6(REAL)
rng (L ^\ L) is V1() V153() V154() V155() Element of K6(REAL)
Z /* ((L + r) ^\ 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))
Z /* (r ^\ 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))
(Z /* ((L + r) ^\ L)) - (Z /* (r ^\ 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 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 + r) ^\ L)) - (Z /* (r ^\ L))) . s1 is Element of the carrier of F
(Z /* ((L + r) ^\ L)) . s1 is Element of the carrier of F
(Z /* (r ^\ L)) . s1 is Element of the carrier of F
((Z /* ((L + r) ^\ L)) . s1) - ((Z /* (r ^\ L)) . s1) is Element of the carrier of F
((L + r) ^\ L) . s1 is V11() real ext-real Element of REAL
Z /. (((L + r) ^\ L) . s1) is Element of the carrier of F
(Z /. (((L + r) ^\ L) . s1)) - ((Z /* (r ^\ L)) . s1) is Element of the carrier of F
(r ^\ L) . s1 is V11() real ext-real Element of REAL
Z /. ((r ^\ L) . s1) is Element of the carrier of F
(Z /. (((L + r) ^\ L) . s1)) - (Z /. ((r ^\ L) . s1)) is Element of the carrier of F
(L ^\ L) . s1 is V11() real ext-real Element of REAL
R . ((L ^\ L) . s1) is Element of the carrier of F
p /. ((L ^\ L) . s1) is Element of the carrier of F
(R . ((L ^\ L) . s1)) + (p /. ((L ^\ L) . s1)) is Element of the carrier of F
(R /* (L ^\ L)) . s1 is Element of the carrier of F
((R /* (L ^\ L)) . s1) + (p /. ((L ^\ L) . s1)) is Element of the carrier of F
(p /* (L ^\ L)) . s1 is Element of the carrier of F
((R /* (L ^\ L)) . s1) + ((p /* (L ^\ L)) . s1) is Element of the carrier of F
((R /* (L ^\ L)) + (p /* (L ^\ L))) . s1 is Element of the carrier of F
(Z /* (L + r)) ^\ L is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of Z /* (L + r)
((Z /* (L + r)) ^\ L) - (Z /* (r ^\ 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) ") (#) (((Z /* (L + r)) ^\ L) - (Z /* (r ^\ 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))
(Z /* r) ^\ L is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of Z /* r
((Z /* (L + r)) ^\ L) - ((Z /* r) ^\ 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) ") (#) (((Z /* (L + r)) ^\ L) - ((Z /* r) ^\ 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))
((Z /* (L + r)) - (Z /* r)) ^\ L is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of (Z /* (L + r)) - (Z /* r)
((L ^\ L) ") (#) (((Z /* (L + r)) - (Z /* r)) ^\ 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 subsequence of L "
((L ") ^\ L) (#) (((Z /* (L + r)) - (Z /* r)) ^\ 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 ") (#) ((Z /* (L + r)) - (Z /* r))) ^\ L is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of (L ") (#) ((Z /* (L + r)) - (Z /* r))
s1 is V11() real ext-real Element of REAL
Z /. s1 is Element of the carrier of F
(Z /. s1) - (Z /. f) is Element of the carrier of F
s1 - f is V11() real ext-real Element of REAL
R . (s1 - f) is Element of the carrier of F
p /. (s1 - f) is Element of the carrier of F
(R . (s1 - f)) + (p /. (s1 - 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 Element of K6(K7(REAL, the carrier of F))
(F,f,Z) 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))
f + x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
(F,(f + x),Z) is Element of the carrier of F
(F,x,Z) is Element of the carrier of F
(F,f,Z) + (F,x,Z) is Element of the carrier of F
dom f is V153() V154() V155() Element of K6(REAL)
f /. Z is Element of the carrier of F
R is V153() V154() V155() open Neighbourhood of Z
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))
dom x is V153() V154() V155() Element of K6(REAL)
x /. Z is Element of the carrier of F
r is V153() V154() V155() open Neighbourhood of Z
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
L + N is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
L + x0 is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom L is V1() V153() V154() V155() Element of K6(REAL)
dom x0 is V1() V153() V154() V155() Element of K6(REAL)
p is V153() V154() V155() open Neighbourhood of Z
p /\ p is V153() V154() V155() Element of K6(REAL)
(dom f) /\ (dom x) is V153() V154() V155() Element of K6(REAL)
dom (f + x) is V153() V154() V155() Element of K6(REAL)
dom (L + N) is V153() V154() V155() Element of K6(REAL)
dom (L + x0) is V153() V154() V155() Element of K6(REAL)
s1 is V11() real ext-real Element of REAL
(f + x) /. s1 is Element of the carrier of F
(f + x) /. Z is Element of the carrier of F
((f + x) /. s1) - ((f + x) /. Z) is Element of the carrier of F
f /. s1 is Element of the carrier of F
x /. s1 is Element of the carrier of F
(f /. s1) + (x /. s1) is Element of the carrier of F
((f /. s1) + (x /. s1)) - ((f + x) /. Z) is Element of the carrier of F
(f /. Z) + (x /. Z) is Element of the carrier of F
((f /. s1) + (x /. s1)) - ((f /. Z) + (x /. Z)) is Element of the carrier of F
(x /. s1) - ((f /. Z) + (x /. Z)) is Element of the carrier of F
(f /. s1) + ((x /. s1) - ((f /. Z) + (x /. Z))) is Element of the carrier of F
(x /. s1) - (x /. Z) is Element of the carrier of F
((x /. s1) - (x /. Z)) - (f /. Z) is Element of the carrier of F
(f /. s1) + (((x /. s1) - (x /. Z)) - (f /. Z)) is Element of the carrier of F
(f /. s1) + ((x /. s1) - (x /. Z)) is Element of the carrier of F
((f /. s1) + ((x /. s1) - (x /. Z))) - (f /. Z) is Element of the carrier of F
(f /. s1) - (f /. Z) is Element of the carrier of F
((x /. s1) - (x /. Z)) + ((f /. s1) - (f /. Z)) is Element of the carrier of F
s1 - Z is V11() real ext-real Element of REAL
L . (s1 - Z) is Element of the carrier of F
L /. (s1 - Z) is Element of the carrier of F
(L . (s1 - Z)) + (L /. (s1 - Z)) is Element of the carrier of F
((L . (s1 - Z)) + (L /. (s1 - Z))) + ((x /. s1) - (x /. Z)) is Element of the carrier of F
x0 . (s1 - Z) is Element of the carrier of F
N /. (s1 - Z) is Element of the carrier of F
(x0 . (s1 - Z)) + (N /. (s1 - Z)) is Element of the carrier of F
((L . (s1 - Z)) + (L /. (s1 - Z))) + ((x0 . (s1 - Z)) + (N /. (s1 - Z))) is Element of the carrier of F
((L . (s1 - Z)) + (L /. (s1 - Z))) + (x0 . (s1 - Z)) is Element of the carrier of F
(((L . (s1 - Z)) + (L /. (s1 - Z))) + (x0 . (s1 - Z))) + (N /. (s1 - Z)) is Element of the carrier of F
(L . (s1 - Z)) + (x0 . (s1 - Z)) is Element of the carrier of F
((L . (s1 - Z)) + (x0 . (s1 - Z))) + (L /. (s1 - Z)) is Element of the carrier of F
(((L . (s1 - Z)) + (x0 . (s1 - Z))) + (L /. (s1 - Z))) + (N /. (s1 - Z)) is Element of the carrier of F
L /. (s1 - Z) is Element of the carrier of F
x0 /. (s1 - Z) is Element of the carrier of F
(L /. (s1 - Z)) + (x0 /. (s1 - Z)) is Element of the carrier of F
(L /. (s1 - Z)) + (N /. (s1 - Z)) is Element of the carrier of F
((L /. (s1 - Z)) + (x0 /. (s1 - Z))) + ((L /. (s1 - Z)) + (N /. (s1 - Z))) is Element of 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))
R /. (s1 - Z) is Element of the carrier of F
R . (s1 - Z) is Element of the carrier of F
(R /. (s1 - Z)) + ((L /. (s1 - Z)) + (N /. (s1 - Z))) is Element of 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 /. (s1 - Z) is Element of the carrier of F
(R . (s1 - Z)) + (L /. (s1 - Z)) is Element of the carrier of F
R . 1 is Element of the carrier of F
R /. 1 is Element of the carrier of F
L /. 1 is Element of the carrier of F
x0 /. 1 is Element of the carrier of F
(L /. 1) + (x0 /. 1) is Element of the carrier of F
L . 1 is Element of the carrier of F
(L . 1) + (x0 /. 1) is Element of the carrier of F
x0 . 1 is Element of the carrier of F
(L . 1) + (x0 . 1) is Element of the carrier of F
(F,f,Z) + (x0 . 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 V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
(F,f,Z) 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))
f - x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
(F,(f - x),Z) is Element of the carrier of F
(F,x,Z) is Element of the carrier of F
(F,f,Z) - (F,x,Z) is Element of the carrier of F
dom f is V153() V154() V155() Element of K6(REAL)
f /. Z is Element of the carrier of F
R is V153() V154() V155() open Neighbourhood of Z
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))
dom x is V153() V154() V155() Element of K6(REAL)
x /. Z is Element of the carrier of F
r is V153() V154() V155() open Neighbourhood of Z
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
L - N is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
L - x0 is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom L is V1() V153() V154() V155() Element of K6(REAL)
dom x0 is V1() V153() V154() V155() Element of K6(REAL)
p is V153() V154() V155() open Neighbourhood of Z
p /\ p is V153() V154() V155() Element of K6(REAL)
(dom f) /\ (dom x) is V153() V154() V155() Element of K6(REAL)
dom (f - x) is V153() V154() V155() Element of K6(REAL)
dom (L - N) is V153() V154() V155() Element of K6(REAL)
dom (L - x0) is V153() V154() V155() Element of K6(REAL)
s1 is V11() real ext-real Element of REAL
(f - x) /. s1 is Element of the carrier of F
(f - x) /. Z is Element of the carrier of F
((f - x) /. s1) - ((f - x) /. Z) is Element of the carrier of F
f /. s1 is Element of the carrier of F
x /. s1 is Element of the carrier of F
(f /. s1) - (x /. s1) is Element of the carrier of F
((f /. s1) - (x /. s1)) - ((f - x) /. Z) is Element of the carrier of F
(f /. Z) - (x /. Z) is Element of the carrier of F
((f /. s1) - (x /. s1)) - ((f /. Z) - (x /. Z)) is Element of the carrier of F
(x /. s1) + ((f /. Z) - (x /. Z)) is Element of the carrier of F
(f /. s1) - ((x /. s1) + ((f /. Z) - (x /. Z))) is Element of the carrier of F
(x /. s1) + (f /. Z) is Element of the carrier of F
((x /. s1) + (f /. Z)) - (x /. Z) is Element of the carrier of F
(f /. s1) - (((x /. s1) + (f /. Z)) - (x /. Z)) is Element of the carrier of F
(x /. s1) - (x /. Z) is Element of the carrier of F
(f /. Z) + ((x /. s1) - (x /. Z)) is Element of the carrier of F
(f /. s1) - ((f /. Z) + ((x /. s1) - (x /. Z))) is Element of the carrier of F
(f /. s1) - (f /. Z) is Element of the carrier of F
((f /. s1) - (f /. Z)) - ((x /. s1) - (x /. Z)) is Element of the carrier of F
s1 - Z is V11() real ext-real Element of REAL
L . (s1 - Z) is Element of the carrier of F
L /. (s1 - Z) is Element of the carrier of F
(L . (s1 - Z)) + (L /. (s1 - Z)) is Element of the carrier of F
((L . (s1 - Z)) + (L /. (s1 - Z))) - ((x /. s1) - (x /. Z)) is Element of the carrier of F
x0 . (s1 - Z) is Element of the carrier of F
N /. (s1 - Z) is Element of the carrier of F
(x0 . (s1 - Z)) + (N /. (s1 - Z)) is Element of the carrier of F
((L . (s1 - Z)) + (L /. (s1 - Z))) - ((x0 . (s1 - Z)) + (N /. (s1 - Z))) is Element of the carrier of F
(L /. (s1 - Z)) - ((x0 . (s1 - Z)) + (N /. (s1 - Z))) is Element of the carrier of F
(L . (s1 - Z)) + ((L /. (s1 - Z)) - ((x0 . (s1 - Z)) + (N /. (s1 - Z)))) is Element of the carrier of F
(L /. (s1 - Z)) - (N /. (s1 - Z)) is Element of the carrier of F
((L /. (s1 - Z)) - (N /. (s1 - Z))) - (x0 . (s1 - Z)) is Element of the carrier of F
(L . (s1 - Z)) + (((L /. (s1 - Z)) - (N /. (s1 - Z))) - (x0 . (s1 - Z))) is Element of the carrier of F
(L . (s1 - Z)) + ((L /. (s1 - Z)) - (N /. (s1 - Z))) is Element of the carrier of F
((L . (s1 - Z)) + ((L /. (s1 - Z)) - (N /. (s1 - Z)))) - (x0 . (s1 - Z)) is Element of the carrier of F
L /. (s1 - Z) is Element of the carrier of F
x0 /. (s1 - Z) is Element of the carrier of F
(L /. (s1 - Z)) - (x0 /. (s1 - Z)) is Element of the carrier of F
((L /. (s1 - Z)) - (x0 /. (s1 - Z))) + ((L /. (s1 - Z)) - (N /. (s1 - Z))) is Element of 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))
R /. (s1 - Z) is Element of the carrier of F
R . (s1 - Z) is Element of the carrier of F
(R /. (s1 - Z)) + ((L /. (s1 - Z)) - (N /. (s1 - Z))) is Element of 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 /. (s1 - Z) is Element of the carrier of F
(R . (s1 - Z)) + (L /. (s1 - Z)) is Element of the carrier of F
R . 1 is Element of the carrier of F
R /. 1 is Element of the carrier of F
L /. 1 is Element of the carrier of F
x0 /. 1 is Element of the carrier of F
(L /. 1) - (x0 /. 1) is Element of the carrier of F
L . 1 is Element of the carrier of F
(L . 1) - (x0 /. 1) is Element of the carrier of F
x0 . 1 is Element of the carrier of F
(L . 1) - (x0 . 1) is Element of the carrier of F
(F,f,Z) - (x0 . 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 V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
(F,f,Z) is Element of the carrier of F
x is V11() real ext-real Element of REAL
x (#) f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
(F,(x (#) f),Z) is Element of the carrier of F
x * (F,f,Z) is Element of the carrier of F
dom f is V153() V154() V155() Element of K6(REAL)
f /. Z is Element of the carrier of F
R is V153() V154() V155() open Neighbourhood of Z
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))
x (#) L is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
x (#) L is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom L is V1() V153() V154() V155() Element of K6(REAL)
dom (x (#) f) is V153() V154() V155() Element of K6(REAL)
dom (x (#) L) is V153() V154() V155() Element of K6(REAL)
dom (x (#) L) is V153() V154() V155() Element of K6(REAL)
N is V11() real ext-real Element of REAL
(x (#) f) /. N is Element of the carrier of F
(x (#) f) /. Z is Element of the carrier of F
((x (#) f) /. N) - ((x (#) f) /. Z) is Element of the carrier of F
f /. N is Element of the carrier of F
x * (f /. N) is Element of the carrier of F
(x * (f /. N)) - ((x (#) f) /. Z) is Element of the carrier of F
x * (f /. Z) is Element of the carrier of F
(x * (f /. N)) - (x * (f /. Z)) is Element of the carrier of F
(f /. N) - (f /. Z) is Element of the carrier of F
x * ((f /. N) - (f /. Z)) is Element of the carrier of F
N - Z is V11() real ext-real Element of REAL
L . (N - Z) is Element of the carrier of F
L /. (N - Z) is Element of the carrier of F
(L . (N - Z)) + (L /. (N - Z)) is Element of the carrier of F
x * ((L . (N - Z)) + (L /. (N - Z))) is Element of the carrier of F
L /. (N - Z) is Element of the carrier of F
x * (L /. (N - Z)) is Element of the carrier of F
x * (L /. (N - Z)) is Element of the carrier of F
(x * (L /. (N - Z))) + (x * (L /. (N - Z))) is Element of the carrier of F
x0 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 /. (N - Z) is Element of the carrier of F
x0 . (N - Z) is Element of the carrier of F
(x0 /. (N - Z)) + (x * (L /. (N - Z))) 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))
r /. (N - Z) is Element of the carrier of F
(x0 . (N - Z)) + (r /. (N - Z)) is Element of the carrier of F
x0 . 1 is Element of the carrier of F
x0 /. 1 is Element of the carrier of F
L /. 1 is Element of the carrier of F
x * (L /. 1) is Element of the carrier of F
L . 1 is Element of the carrier of F
x * (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 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))
x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
f + x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom (f + x) is V153() V154() V155() Element of K6(REAL)
(F,(f + x),Z) is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
R is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
(F,(f + x),Z) . R is set
(F,f,R) is Element of the carrier of F
(F,x,R) is Element of the carrier of F
(F,f,R) + (F,x,R) is Element of the carrier of F
(F,(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 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))
x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
f - x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom (f - x) is V153() V154() V155() Element of K6(REAL)
(F,(f - x),Z) is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
R is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
(F,(f - x),Z) . R is set
(F,f,R) is Element of the carrier of F
(F,x,R) is Element of the carrier of F
(F,f,R) - (F,x,R) is Element of the carrier of F
(F,(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 V11() real ext-real Element of REAL
f is V153() V154() V155() open Element of K6(REAL)
x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
Z (#) x is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom (Z (#) x) is V153() V154() V155() Element of K6(REAL)
(F,(Z (#) x),f) is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
R is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
(F,(Z (#) x),f) . R is set
(F,x,R) is Element of the carrier of F
Z * (F,x,R) is Element of the carrier of F
(F,(Z (#) 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
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)
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))
(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 V11() real ext-real Element of REAL
(REAL --> (0. F)) . L is Element of the carrier of F
L * (0. F) is Element of the carrier of F
Z /\ (dom f) is V153() V154() V155() Element of K6(REAL)
r is Element of the carrier of F
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 set
N is V153() V154() V155() open Neighbourhood of x0
f /. x0 is Element of 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
(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 Element of the carrier of F
f is Element of the carrier of F
x is V153() V154() V155() open 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)
(F,R,x) is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
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))
dom (REAL --> (0. F)) is V1() V153() V154() V155() Element of K6(REAL)
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))
rng L is V1() V153() V154() V155() Element of K6(REAL)
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(REAL --> (0. F)) /* 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))
K7(NAT, the carrier of F) is V1() V13() set
K6(K7(NAT, the carrier of F)) is V1() set
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 ") (#) ((REAL --> (0. F)) /* 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 ") (#) ((REAL --> (0. F)) /* L)) . r is Element of the carrier of F
((REAL --> (0. F)) /* L) . r is Element of the carrier of F
(L ") . r is V11() real ext-real Element of REAL
((L ") . r) * (((REAL --> (0. F)) /* L) . r) is Element of the carrier of F
L . r is V11() real ext-real Element of REAL
(REAL --> (0. F)) /. (L . r) is Element of the carrier of F
(REAL --> (0. F)) . (L . r) is Element of the carrier of F
((L ") . r) * ((REAL --> (0. F)) /. (L . r)) is Element of the carrier of F
((L ") (#) ((REAL --> (0. F)) /* L)) . 0 is Element of the carrier of F
lim ((L ") (#) ((REAL --> (0. F)) /* L)) is Element of the carrier of F
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)
x0 is V11() real ext-real Element of REAL
r . x0 is set
x0 * Z is Element of the carrier of F
N is V11() real ext-real Element of REAL
L is V153() V154() V155() open Neighbourhood of N
R /. N is Element of the carrier of F
x0 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
R /. R is Element of the carrier of F
(R /. R) - (R /. N) is Element of the carrier of F
R - N is V11() real ext-real Element of REAL
x0 . (R - N) is Element of the carrier of F
L /. (R - N) is Element of the carrier of F
(x0 . (R - N)) + (L /. (R - N)) is Element of the carrier of F
L . (R - N) is set
R * Z is Element of the carrier of F
(R * Z) + f is Element of the carrier of F
((R * Z) + f) - (R /. N) is Element of the carrier of F
N * Z is Element of the carrier of F
(N * Z) + f is Element of the carrier of F
((R * Z) + f) - ((N * Z) + f) is Element of the carrier of F
((R * Z) + f) - (N * Z) is Element of the carrier of F
(((R * Z) + f) - (N * Z)) - f is Element of the carrier of F
(R * Z) - (N * Z) is Element of the carrier of F
f + ((R * Z) - (N * Z)) is Element of the carrier of F
(f + ((R * Z) - (N * Z))) - f is Element of the carrier of F
f - f is Element of the carrier of F
((R * Z) - (N * Z)) + (f - f) is Element of the carrier of F
((R * Z) - (N * Z)) + (0. F) is Element of the carrier of F
(R - N) * Z is Element of the carrier of F
((R - N) * Z) + (0. F) is Element of the carrier of F
N is V11() real ext-real Element of REAL
(F,R,x) . N is set
L is V153() V154() V155() open Neighbourhood of N
R /. N is Element of the carrier of F
R is V11() real ext-real Element of REAL
R /. R is Element of the carrier of F
(R /. R) - (R /. N) is Element of the carrier of F
R - N is V11() real ext-real Element of REAL
x0 . (R - N) is Element of the carrier of F
L /. (R - N) is Element of the carrier of F
(x0 . (R - N)) + (L /. (R - N)) is Element of the carrier of F
L . (R - N) is set
R * Z is Element of the carrier of F
(R * Z) + f is Element of the carrier of F
((R * Z) + f) - (R /. N) is Element of the carrier of F
N * Z is Element of the carrier of F
(N * Z) + f is Element of the carrier of F
((R * Z) + f) - ((N * Z) + f) is Element of the carrier of F
((R * Z) + f) - (N * Z) is Element of the carrier of F
(((R * Z) + f) - (N * Z)) - f is Element of the carrier of F
(R * Z) - (N * Z) is Element of the carrier of F
f + ((R * Z) - (N * Z)) is Element of the carrier of F
(f + ((R * Z) - (N * Z))) - f is Element of the carrier of F
f - f is Element of the carrier of F
((R * Z) - (N * Z)) + (f - f) is Element of the carrier of F
((R * Z) - (N * Z)) + (0. F) is Element of the carrier of F
(R - N) * Z is Element of the carrier of F
((R - N) * Z) + (0. F) is Element of the carrier of F
(F,R,N) is Element of the carrier of F
x0 . 1 is Element of the carrier of F
1 * Z 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 V11() real ext-real Element of REAL
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 V11() real ext-real set
f - R is V11() real ext-real Element of REAL
f + R is V11() real ext-real Element of REAL
].(f - R),(f + R).[ is V153() V154() V155() open Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - R & not f + R <= b₁ ) } is set
NAT --> f is V1() T-Sequence-like 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))
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))
rng L is V1() V153() V154() V155() Element of K6(REAL)
lim L 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
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 ^\ r is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of L
N 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 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))
x0 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 x0 is V1() V153() V154() V155() Element of K6(REAL)
{f} is V153() V154() V155() set
L is 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 ^\ r) . R is V11() real ext-real Element of REAL
R + 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 + r) is V11() real ext-real Element of REAL
L is 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
x0 . R is V11() real ext-real Element of REAL
R + 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 + r) is V11() real ext-real Element of REAL
L 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
p 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 /* x0 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 /* x0) . p is Element of the carrier of F
((Z /* x0) . p) - (Z /. f) is Element of the carrier of F
||.(((Z /* x0) . p) - (Z /. f)).|| is V11() real ext-real non negative Element of REAL
x0 . p is V11() real ext-real Element of REAL
Z /. (x0 . p) is Element of the carrier of F
(Z /. (x0 . p)) - (Z /. f) is Element of the carrier of F
||.((Z /. (x0 . p)) - (Z /. f)).|| is V11() real ext-real non negative Element of REAL
p + 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 . (p + r) is V11() real ext-real Element of REAL
Z /. (L . (p + r)) is Element of the carrier of F
(Z /. (L . (p + r))) - (Z /. f) is Element of the carrier of F
||.((Z /. (L . (p + r))) - (Z /. f)).|| is V11() real ext-real non negative Element of REAL
(Z /. f) - (Z /. f) is Element of the carrier of F
||.((Z /. f) - (Z /. f)).|| is V11() real ext-real non negative Element of REAL
0. F is V53(F) Element of the carrier of F
||.(0. F).|| 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
lim L is V11() real ext-real Element of REAL
L . 0 is V11() real ext-real Element of REAL
lim N is V11() real ext-real Element of REAL
f - f is V11() real ext-real Element of REAL
N ^\ r is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of N
lim (N ^\ r) 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
N . L is V11() real ext-real Element of REAL
L . L is V11() real ext-real Element of REAL
L . L is V11() real ext-real Element of REAL
(L . L) - (L . L) 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
(N ^\ r) . L is V11() real ext-real Element of REAL
L + 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
N . (L + r) is V11() real ext-real Element of REAL
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 + x0 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 /* (L + x0) 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 + x0)) - (Z /* x0) 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 + x0)) - (Z /* x0)) + (Z /* x0) 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 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 + x0)) - (Z /* x0)) + (Z /* x0)) . R is Element of the carrier of F
((Z /* (L + x0)) - (Z /* x0)) . R is Element of the carrier of F
(Z /* x0) . R is Element of the carrier of F
(((Z /* (L + x0)) - (Z /* x0)) . R) + ((Z /* x0) . R) is Element of the carrier of F
(Z /* (L + x0)) . R is Element of the carrier of F
((Z /* (L + x0)) . R) - ((Z /* x0) . R) is Element of the carrier of F
(((Z /* (L + x0)) . R) - ((Z /* x0) . R)) + ((Z /* x0) . R) is Element of the carrier of F
((Z /* x0) . R) - ((Z /* x0) . R) is Element of the carrier of F
((Z /* (L + x0)) . R) - (((Z /* x0) . R) - ((Z /* x0) . R)) is Element of the carrier of F
((Z /* (L + x0)) . R) - (0. F) is Element of the carrier of F
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 + x0) . R is V11() real ext-real Element of REAL
(L - 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) + L) ^\ r is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (L - L) + L
(((L - L) + L) ^\ r) . R is V11() real ext-real Element of REAL
R + 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 - L) + L) . (R + r) is V11() real ext-real Element of REAL
(L - L) . (R + r) is V11() real ext-real Element of REAL
L . (R + r) is V11() real ext-real Element of REAL
((L - L) . (R + r)) + (L . (R + r)) is V11() real ext-real Element of REAL
L . (R + r) is V11() real ext-real Element of REAL
(L . (R + r)) - (L . (R + r)) is V11() real ext-real Element of REAL
((L . (R + r)) - (L . (R + r))) + (L . (R + r)) is V11() real ext-real Element of REAL
L ^\ r is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of L
(L ^\ r) . R is V11() real ext-real Element of 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))
Z /* 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))
(Z /* L) ^\ r is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total subsequence of Z /* L
R is set
rng (L + x0) is V1() V153() V154() V155() Element of K6(REAL)
p 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 + x0) . p is V11() real ext-real Element of REAL
(((L - L) + L) ^\ r) . p is V11() real ext-real Element of REAL
p + 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 - L) + L) . (p + r) is V11() real ext-real Element of REAL
(L - L) . (p + r) is V11() real ext-real Element of REAL
L . (p + r) is V11() real ext-real Element of REAL
((L - L) . (p + r)) + (L . (p + r)) is V11() real ext-real Element of REAL
L . (p + r) is V11() real ext-real Element of REAL
(L . (p + r)) - (L . (p + r)) is V11() real ext-real Element of REAL
((L . (p + r)) - (L . (p + r))) + (L . (p + r)) is V11() real ext-real Element of REAL
r + p 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 + p) is V11() real ext-real Element of REAL
((L + x0) . p) - f is V11() real ext-real Element of REAL
abs (((L + x0) . p) - f) is V11() real ext-real Element of 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))
(L ") (#) ((Z /* (L + x0)) - (Z /* x0)) 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 ") (#) ((Z /* (L + x0)) - (Z /* x0))) 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 ") (#) ((Z /* (L + x0)) - (Z /* x0)))) is Element of the carrier of F
lim ((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) is Element of the carrier of F
0 * (lim ((L ") (#) ((Z /* (L + x0)) - (Z /* x0)))) is Element of the carrier of F
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 is V11() real ext-real Element of REAL
(L (#) ((L ") (#) ((Z /* (L + x0)) - (Z /* x0)))) . R is Element of the carrier of F
((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) . R is Element of the carrier of F
(L . R) * (((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) . R) is Element of the carrier of F
((Z /* (L + x0)) - (Z /* x0)) . R is Element of the carrier of F
(L ") . R is V11() real ext-real Element of REAL
((L ") . R) * (((Z /* (L + x0)) - (Z /* x0)) . R) is Element of the carrier of F
(L . R) * (((L ") . R) * (((Z /* (L + x0)) - (Z /* x0)) . R)) is Element of the carrier of F
(L . R) " is V11() real ext-real Element of REAL
((L . R) ") * (((Z /* (L + x0)) - (Z /* x0)) . R) is Element of the carrier of F
(L . R) * (((L . R) ") * (((Z /* (L + x0)) - (Z /* x0)) . R)) is Element of the carrier of F
(L . R) * ((L . R) ") is V11() real ext-real Element of REAL
((L . R) * ((L . R) ")) * (((Z /* (L + x0)) - (Z /* x0)) . R) is Element of the carrier of F
1 * (((Z /* (L + x0)) - (Z /* x0)) . R) is Element of the carrier of F
lim (Z /* x0) is Element of the carrier of F
lim (((Z /* (L + x0)) - (Z /* x0)) + (Z /* x0)) is Element of the carrier of F
(0. F) + (Z /. f) is Element of the carrier of F
lim (Z /* L) 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 set
f is V13() V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, 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 set
dom (f | Z) is Element of K6(Z)
K6(Z) 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 V153() V154() V155() open Element of K6(REAL)
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 V11() real ext-real Element of REAL
x | 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 (x | Z) is Element of K6(Z)
K6(Z) is V1() set
(x | Z) /. R is Element of the carrier of F
L is V153() V154() V155() open Neighbourhood of R
L is V153() V154() V155() open Neighbourhood of R
r is V153() V154() V155() open Neighbourhood of R
(dom x) /\ Z is V153() V154() V155() Element of K6(REAL)
(dom x) /\ f is V153() V154() V155() Element of K6(REAL)
x | f is V13() V16( REAL ) V16(f) V16( REAL ) V17( the carrier of F) Function-like Element of K6(K7(REAL, the carrier of F))
dom (x | f) is V153() V154() V155() Element of K6(f)
K6(f) is V1() set
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
x0 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))
N is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
(x | f) /. R is Element of the carrier of F
L is V11() real ext-real Element of REAL
(x | f) /. L is Element of the carrier of F
((x | f) /. L) - ((x | f) /. R) is Element of the carrier of F
L - R is V11() real ext-real Element of REAL
x0 . (L - R) is Element of the carrier of F
N /. (L - R) is Element of the carrier of F
(x0 . (L - R)) + (N /. (L - R)) is Element of the carrier of F
(x | Z) /. L is Element of the carrier of F
((x | Z) /. L) - ((x | Z) /. R) is Element of the carrier of F
x /. R is Element of the carrier of F
((x | Z) /. L) - (x /. R) is Element of the carrier of F
x /. L is Element of the carrier of F
(x /. L) - (x /. R) is Element of the carrier of F
(x /. L) - ((x | f) /. R) is Element of the carrier of F
{} REAL is V1() proper 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 K6(REAL)
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))
rng F is V1() V153() V154() V155() set
lim F is V11() real ext-real Element of REAL
rng F 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
0. F is V53(F) Element of the carrier of F
[#] REAL is V1() non proper V153() V154() V155() Element of K6(REAL)
([#] REAL) ` is V153() V154() V155() Element of K6(REAL)
K4(REAL,([#] REAL)) is V153() V154() V155() set
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 V11() real ext-real Element of REAL
(REAL --> (0. F)) . L is Element of the carrier of F
L * (0. F) is Element of the carrier of F
Z is V153() V154() V155() open Element of K6(REAL)
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)
x | 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))
Z /\ (dom x) is V153() V154() V155() Element of K6(REAL)
r is Element of the carrier of F
x0 is V11() real ext-real Element of REAL
x /. x0 is Element of the carrier of F
x . x0 is set
x0 is V11() real ext-real Element of REAL
the V153() V154() V155() open Neighbourhood of x0 is V153() V154() V155() open Neighbourhood of x0
x /. 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
x /. L is Element of the carrier of F
(x /. L) - (x /. 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 - (x /. x0) is Element of the carrier of F
r - r is Element of the carrier of F
the V11() real ext-real Element of REAL is V11() real ext-real Element of REAL
x /. the V11() real ext-real Element of REAL is Element of the carrier of F
N is V153() V154() V155() open Neighbourhood of the V11() real ext-real Element of 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))
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))
R is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
R /. 0 is Element of the carrier of F
p is Element of the carrier of F
(x /. the V11() real ext-real Element of REAL ) - (x /. the V11() real ext-real Element of REAL ) is Element of the carrier of F
the V11() real ext-real Element of REAL - the V11() real ext-real Element of REAL is V11() real ext-real Element of REAL
L . ( the V11() real ext-real Element of REAL - the V11() real ext-real Element of REAL ) is Element of the carrier of F
R /. ( the V11() real ext-real Element of REAL - the V11() real ext-real Element of REAL ) is Element of the carrier of F
(L . ( the V11() real ext-real Element of REAL - the V11() real ext-real Element of REAL )) + (R /. ( the V11() real ext-real Element of REAL - the V11() real ext-real Element of REAL )) is Element of the carrier of F
0 * p is Element of the carrier of F
(0 * p) + (R /. 0) is Element of the carrier of F
(0. F) + (R /. 0) is Element of the carrier of F
cs 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))
cs . 1 is V11() real ext-real Element of REAL
h 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))
R /* h is V1() V13() V16( NAT ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(NAT, the carrier of F))
h " 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))
(h ") (#) (R /* h) 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 ((h ") (#) (R /* h)) is Element of the carrier of F
||.((h ") (#) (R /* h)).|| 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))
M is V11() real ext-real set
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
||.((h ") (#) (R /* h)).|| . z0 is V11() real ext-real Element of REAL
abs (||.((h ") (#) (R /* h)).|| . z0) is V11() real ext-real Element of REAL
((h ") (#) (R /* h)) . z0 is Element of the carrier of F
||.(((h ") (#) (R /* h)) . z0).|| is V11() real ext-real non negative Element of REAL
abs ||.(((h ") (#) (R /* h)) . z0).|| is V11() real ext-real Element of 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
((h ") (#) (R /* h)) . z0 is Element of the carrier of F
||.(((h ") (#) (R /* h)) . z0).|| is V11() real ext-real non negative Element of REAL
(R /* h) . z0 is Element of the carrier of F
(h ") . z0 is V11() real ext-real Element of REAL
((h ") . z0) * ((R /* h) . z0) is Element of the carrier of F
||.(((h ") . z0) * ((R /* h) . z0)).|| is V11() real ext-real non negative Element of REAL
h . z0 is V11() real ext-real Element of REAL
(h . z0) " is V11() real ext-real Element of REAL
((h . z0) ") * ((R /* h) . z0) is Element of the carrier of F
||.(((h . z0) ") * ((R /* h) . z0)).|| is V11() real ext-real non negative Element of REAL
abs (h . z0) is V11() real ext-real Element of REAL
(abs (h . z0)) * ||.(((h . z0) ") * ((R /* h) . z0)).|| is V11() real ext-real Element of REAL
M * (abs (h . z0)) is V11() real ext-real Element of REAL
(h . z0) * (((h . z0) ") * ((R /* h) . z0)) is Element of the carrier of F
||.((h . z0) * (((h . z0) ") * ((R /* h) . z0))).|| is V11() real ext-real non negative Element of REAL
(h . z0) * ((h . z0) ") is V11() real ext-real Element of REAL
((h . z0) * ((h . z0) ")) * ((R /* h) . z0) is Element of the carrier of F
||.(((h . z0) * ((h . z0) ")) * ((R /* h) . z0)).|| is V11() real ext-real non negative Element of REAL
1 * ((R /* h) . z0) is Element of the carrier of F
||.(1 * ((R /* h) . z0)).|| is V11() real ext-real non negative Element of REAL
||.((R /* h) . z0).|| is V11() real ext-real non negative Element of REAL
abs h is V1() V13() V16( NAT ) V17( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))
(abs h) . z0 is V11() real ext-real Element of REAL
M * ((abs h) . z0) is V11() real ext-real Element of REAL
M (#) (abs h) 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))
(M (#) (abs h)) . z0 is V11() real ext-real Element of REAL
lim h 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
z0 is V11() real ext-real Element of REAL
lim (abs h) is V11() real ext-real Element of REAL
abs z0 is V11() real ext-real Element of REAL
lim (M (#) (abs h)) is V11() real ext-real Element of REAL
M * z0 is V11() real ext-real Element of REAL
lim cs is V11() real ext-real Element of REAL
lim (R /* h) is Element of the carrier of F
dom R is V153() V154() V155() Element of K6(REAL)
s1 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 s1 is V1() V153() V154() V155() Element of K6(REAL)
lim s1 is V11() real ext-real Element of REAL
R /* 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 (R /* s1) 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
[#] REAL is V1() non proper V153() V154() V155() Element of K6(REAL)
([#] REAL) ` is V153() V154() V155() Element of K6(REAL)
K4(REAL,([#] REAL)) is V153() V154() V155() 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))
f is V1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total Element of K6(K7(REAL, the carrier of F))
Z is V153() V154() V155() open Element of K6(REAL)
dom f is V1() V153() V154() V155() Element of K6(REAL)
x is V11() real ext-real Element of REAL
f /. x is Element of the carrier of F
f . x is Element of the carrier of F
x * (0. F) is Element of the carrier of F
(x * (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 V153() V154() V155() open Element of K6(REAL)
f is V13() V16( REAL ) V17( the carrier of F) Function-like (F) Element of K6(K7(REAL, the carrier of F))
dom f is V153() V154() V155() Element of K6(REAL)