:: NDIFF_1 semantic presentation

REAL is V1() V49() V170() V171() V172() V176() set
NAT is V1() epsilon-transitive epsilon-connected ordinal V170() V171() V172() V173() V174() V175() V176() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V49() V170() V176() set

K6(K7(REAL,REAL)) is set

K6(omega) is set
K6(NAT) is set

K6(K7(NAT,REAL)) is set

K6( the carrier of Linear_Space_of_RealSequences) is set

RAT is V1() V49() V170() V171() V172() V173() V176() set
INT is V1() V49() V170() V171() V172() V173() V174() V176() set

K6(K7(COMPLEX,COMPLEX)) is set

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

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

K6(K7(RAT,RAT)) is set

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

K6(K7(INT,INT)) is set

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

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

0c is set

- 1 is V11() real ext-real non positive Element of REAL
K39(0) is V11() real ext-real set

the carrier of T is V1() set
S is Element of the carrier of T
f is Neighbourhood of S
x0 is Neighbourhood of S
N is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not N <= ||.(b1 - S).|| } is set
L is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not L <= ||.(b1 - S).|| } is set
min (N,L) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not min (N,L) <= ||.(b1 - S).|| } is set
K6( the carrier of T) is set
s1 is set
N2 is Element of the carrier of T
N2 - S is Element of the carrier of T
- S is Element of the carrier of T
K192(T,N2,(- S)) is Element of the carrier of T
||.(N2 - S).|| is V11() real ext-real Element of REAL
s1 is set
N2 is Element of the carrier of T
N2 - S is Element of the carrier of T
- S is Element of the carrier of T
K192(T,N2,(- S)) is Element of the carrier of T
||.(N2 - S).|| is V11() real ext-real Element of REAL

the carrier of T is V1() set
K6( the carrier of T) is set
S is Element of K6( the carrier of T)
S ` is Element of K6( the carrier of T)
K4( the carrier of T,S) is set
f is Element of the carrier of T
{ b1 where b1 is Element of the carrier of T : not 1 / (a1 + 1) <= ||.(b1 - f).|| } is set
x0 is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not x0 <= ||.(b1 - f).|| } is set
L is set
R is Element of the carrier of T
R - f is Element of the carrier of T
- f is Element of the carrier of T
K192(T,R,(- f)) is Element of the carrier of T
||.(R - f).|| is V11() real ext-real Element of REAL
s1 is Element of the carrier of T

1 / (x0 + 1) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not 1 / (x0 + 1) <= ||.(b1 - f).|| } is set
(x0 + 1) " is V11() real ext-real Element of REAL
1 * ((x0 + 1) ") is V11() real ext-real Element of REAL
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng x0 is Element of K6( the carrier of T)
N is set
dom x0 is V170() V171() V172() V173() V174() V175() Element of K6(NAT)
L is set
x0 . L is set

x0 . R is Element of the carrier of T
N is V11() real ext-real Element of REAL
N " is V11() real ext-real Element of REAL

(N ") + 0 is V11() real ext-real Element of REAL
1 / (N ") is V11() real ext-real Element of REAL
1 / (L + 1) is V11() real ext-real Element of REAL

x0 . s1 is Element of the carrier of T
1 / (s1 + 1) is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not 1 / (s1 + 1) <= ||.(b1 - f).|| } is set
1 / (R + 1) is V11() real ext-real Element of REAL
(x0 . s1) - f is Element of the carrier of T
K192(T,(x0 . s1),(- f)) is Element of the carrier of T
||.((x0 . s1) - f).|| is V11() real ext-real Element of REAL
N2 is Element of the carrier of T
N2 - f is Element of the carrier of T
K192(T,N2,(- f)) is Element of the carrier of T
||.(N2 - f).|| is V11() real ext-real Element of REAL
lim x0 is Element of the carrier of T

the carrier of T is V1() set
K6( the carrier of T) is set
S is Element of K6( the carrier of T)
f is Element of the carrier of T
x0 is Neighbourhood of f
N is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not N <= ||.(b1 - f).|| } is set

the carrier of T is V1() set
K6( the carrier of T) is set
S is Element of K6( the carrier of T)
S ` is Element of K6( the carrier of T)
K4( the carrier of T,S) is set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
f is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng f is Element of K6( the carrier of T)
lim f is Element of the carrier of T
x0 is Neighbourhood of lim f
N is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of T : not N <= ||.(b1 - (lim f)).|| } is set

dom f is V170() V171() V172() V173() V174() V175() Element of K6(NAT)
f . L is Element of the carrier of T
(f . L) - (lim f) is Element of the carrier of T
- (lim f) is Element of the carrier of T
K192(T,(f . L),(- (lim f))) is Element of the carrier of T
||.((f . L) - (lim f)).|| is V11() real ext-real Element of REAL

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

the carrier of f is V1() set
K6( the carrier of f) is set
S is Element of K6( the carrier of T)
x0 is Element of K6( the carrier of f)
N is Element of the carrier of f
T is set
S is ZeroStr
the carrier of S is set
K7(T, the carrier of S) is set
K6(K7(T, the carrier of S)) is set
f is V16() V19(T) V20( the carrier of S) Function-like quasi_total Element of K6(K7(T, the carrier of S))
rng f is Element of K6( the carrier of S)
K6( the carrier of S) is set
NonZero S is Element of K6( the carrier of S)
[#] S is non proper Element of K6( the carrier of S)
0. S is V68(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
{(0. S)} is set
([#] S) \ {(0. S)} is Element of K6( the carrier of S)

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng S is Element of K6( the carrier of T)
K6( the carrier of T) is set
NonZero T is Element of K6( the carrier of T)
[#] T is V1() non proper Element of K6( the carrier of T)
{(0. T)} is set
([#] T) \ {(0. T)} is Element of K6( the carrier of T)
f is set
S . f is set
dom S is V170() V171() V172() V173() V174() V175() Element of K6(NAT)
f is set
rng S is Element of K6( the carrier of T)
K6( the carrier of T) is set
dom S is V170() V171() V172() V173() V174() V175() Element of K6(NAT)
x0 is set
S . x0 is set
{(0. T)} is set
NonZero T is Element of K6( the carrier of T)
[#] T is V1() non proper Element of K6( the carrier of T)
([#] T) \ {(0. T)} is Element of K6( the carrier of T)

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

S . f is Element of the carrier of T
f is set
S . f is set

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
N is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

x0 . L is Element of the carrier of T
N . L is Element of the carrier of T
S . L is Element of the carrier of T
f . L is V11() real ext-real Element of REAL
(f . L) * (S . L) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(f . L),(S . L)) is set

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is Element of the carrier of T

x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
N is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

x0 . L is Element of the carrier of T
N . L is Element of the carrier of T
f . L is V11() real ext-real Element of REAL
(f . L) * S is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(f . L),S) is set

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

(T,S,(f + x0)) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,f) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,x0) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,f) + (T,S,x0) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

(T,S,(f + x0)) . N is Element of the carrier of T
S . N is Element of the carrier of T
(f + x0) . N is V11() real ext-real Element of REAL
((f + x0) . N) * (S . N) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,((f + x0) . N),(S . N)) is set
f . N is V11() real ext-real Element of REAL
x0 . N is V11() real ext-real Element of REAL
(f . N) + (x0 . N) is V11() real ext-real Element of REAL
((f . N) + (x0 . N)) * (S . N) is Element of the carrier of T
K249( the Mult of T,((f . N) + (x0 . N)),(S . N)) is set
(f . N) * (S . N) is Element of the carrier of T
K249( the Mult of T,(f . N),(S . N)) is set
(x0 . N) * (S . N) is Element of the carrier of T
K249( the Mult of T,(x0 . N),(S . N)) is set
((f . N) * (S . N)) + ((x0 . N) * (S . N)) is Element of the carrier of T
(T,S,f) . N is Element of the carrier of T
((T,S,f) . N) + ((x0 . N) * (S . N)) is Element of the carrier of T
(T,S,x0) . N is Element of the carrier of T
((T,S,f) . N) + ((T,S,x0) . N) is Element of the carrier of T
((T,S,f) + (T,S,x0)) . N is Element of the carrier of T

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

f is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
f + x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,(f + x0),S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,x0,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) + (T,x0,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

(T,(f + x0),S) . N is Element of the carrier of T
(f + x0) . N is Element of the carrier of T
S . N is V11() real ext-real Element of REAL
(S . N) * ((f + x0) . N) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(S . N),((f + x0) . N)) is set
f . N is Element of the carrier of T
x0 . N is Element of the carrier of T
(f . N) + (x0 . N) is Element of the carrier of T
(S . N) * ((f . N) + (x0 . N)) is Element of the carrier of T
K249( the Mult of T,(S . N),((f . N) + (x0 . N))) is set
(S . N) * (f . N) is Element of the carrier of T
K249( the Mult of T,(S . N),(f . N)) is set
(S . N) * (x0 . N) is Element of the carrier of T
K249( the Mult of T,(S . N),(x0 . N)) is set
((S . N) * (f . N)) + ((S . N) * (x0 . N)) is Element of the carrier of T
(T,f,S) . N is Element of the carrier of T
((T,f,S) . N) + ((S . N) * (x0 . N)) is Element of the carrier of T
(T,x0,S) . N is Element of the carrier of T
((T,f,S) . N) + ((T,x0,S) . N) is Element of the carrier of T
((T,f,S) + (T,x0,S)) . N is Element of the carrier of T
T is V11() real ext-real Element of REAL

the carrier of S is V1() set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
T * f is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))

(S,f,x0) is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
T * (S,f,x0) is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(S,(T * f),x0) is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))

(T * (S,f,x0)) . N is Element of the carrier of S
(S,f,x0) . N is Element of the carrier of S
T * ((S,f,x0) . N) is Element of the carrier of S
the Mult of S is V16() V19(K7(REAL, the carrier of S)) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of S), the carrier of S))
K7(REAL, the carrier of S) is set
K7(K7(REAL, the carrier of S), the carrier of S) is set
K6(K7(K7(REAL, the carrier of S), the carrier of S)) is set
K249( the Mult of S,T,((S,f,x0) . N)) is set
f . N is Element of the carrier of S
x0 . N is V11() real ext-real Element of REAL
(x0 . N) * (f . N) is Element of the carrier of S
K249( the Mult of S,(x0 . N),(f . N)) is set
T * ((x0 . N) * (f . N)) is Element of the carrier of S
K249( the Mult of S,T,((x0 . N) * (f . N))) is set
T * (x0 . N) is V11() real ext-real Element of REAL
(T * (x0 . N)) * (f . N) is Element of the carrier of S
K249( the Mult of S,(T * (x0 . N)),(f . N)) is set
T * (f . N) is Element of the carrier of S
K249( the Mult of S,T,(f . N)) is set
(x0 . N) * (T * (f . N)) is Element of the carrier of S
K249( the Mult of S,(x0 . N),(T * (f . N))) is set
(T * f) . N is Element of the carrier of S
(x0 . N) * ((T * f) . N) is Element of the carrier of S
K249( the Mult of S,(x0 . N),((T * f) . N)) is set
(S,(T * f),x0) . N is Element of the carrier of S

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

K38(1) is V11() real ext-real non positive set

(T,S,(f - x0)) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,f) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,x0) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,S,f) - (T,S,x0) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

(T,S,(f - x0)) . N is Element of the carrier of T
S . N is Element of the carrier of T

(f + (- x0)) . N is V11() real ext-real Element of REAL
((f + (- x0)) . N) * (S . N) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,((f + (- x0)) . N),(S . N)) is set
f . N is V11() real ext-real Element of REAL
(- x0) . N is V11() real ext-real Element of REAL
(f . N) + ((- x0) . N) is V11() real ext-real Element of REAL
((f . N) + ((- x0) . N)) * (S . N) is Element of the carrier of T
K249( the Mult of T,((f . N) + ((- x0) . N)),(S . N)) is set
x0 . N is V11() real ext-real Element of REAL
- (x0 . N) is V11() real ext-real Element of REAL
(f . N) + (- (x0 . N)) is V11() real ext-real Element of REAL
((f . N) + (- (x0 . N))) * (S . N) is Element of the carrier of T
K249( the Mult of T,((f . N) + (- (x0 . N))),(S . N)) is set
(f . N) - (x0 . N) is V11() real ext-real Element of REAL
((f . N) - (x0 . N)) * (S . N) is Element of the carrier of T
K249( the Mult of T,((f . N) - (x0 . N)),(S . N)) is set
(f . N) * (S . N) is Element of the carrier of T
K249( the Mult of T,(f . N),(S . N)) is set
(x0 . N) * (S . N) is Element of the carrier of T
K249( the Mult of T,(x0 . N),(S . N)) is set
((f . N) * (S . N)) - ((x0 . N) * (S . N)) is Element of the carrier of T
- ((x0 . N) * (S . N)) is Element of the carrier of T
K192(T,((f . N) * (S . N)),(- ((x0 . N) * (S . N)))) is Element of the carrier of T
(T,S,f) . N is Element of the carrier of T
((T,S,f) . N) - ((x0 . N) * (S . N)) is Element of the carrier of T
K192(T,((T,S,f) . N),(- ((x0 . N) * (S . N)))) is Element of the carrier of T
(T,S,x0) . N is Element of the carrier of T
((T,S,f) . N) - ((T,S,x0) . N) is Element of the carrier of T
- ((T,S,x0) . N) is Element of the carrier of T
K192(T,((T,S,f) . N),(- ((T,S,x0) . N))) is Element of the carrier of T
((T,S,f) - (T,S,x0)) . N is Element of the carrier of T

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

f is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
f - x0 is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,(f - x0),S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,x0,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) - (T,x0,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))

(T,(f - x0),S) . N is Element of the carrier of T
(f - x0) . N is Element of the carrier of T
S . N is V11() real ext-real Element of REAL
(S . N) * ((f - x0) . N) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(S . N),((f - x0) . N)) is set
f . N is Element of the carrier of T
x0 . N is Element of the carrier of T
(f . N) - (x0 . N) is Element of the carrier of T
- (x0 . N) is Element of the carrier of T
K192(T,(f . N),(- (x0 . N))) is Element of the carrier of T
(S . N) * ((f . N) - (x0 . N)) is Element of the carrier of T
K249( the Mult of T,(S . N),((f . N) - (x0 . N))) is set
(S . N) * (f . N) is Element of the carrier of T
K249( the Mult of T,(S . N),(f . N)) is set
(S . N) * (x0 . N) is Element of the carrier of T
K249( the Mult of T,(S . N),(x0 . N)) is set
((S . N) * (f . N)) - ((S . N) * (x0 . N)) is Element of the carrier of T
- ((S . N) * (x0 . N)) is Element of the carrier of T
K192(T,((S . N) * (f . N)),(- ((S . N) * (x0 . N)))) is Element of the carrier of T
(T,f,S) . N is Element of the carrier of T
((T,f,S) . N) - ((S . N) * (x0 . N)) is Element of the carrier of T
K192(T,((T,f,S) . N),(- ((S . N) * (x0 . N)))) is Element of the carrier of T
(T,x0,S) . N is Element of the carrier of T
((T,f,S) . N) - ((T,x0,S) . N) is Element of the carrier of T
- ((T,x0,S) . N) is Element of the carrier of T
K192(T,((T,f,S) . N),(- ((T,x0,S) . N))) is Element of the carrier of T
((T,f,S) - (T,x0,S)) . N is Element of the carrier of T

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

f is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
x0 is V11() real ext-real set
N is Element of the carrier of T
L is V11() real ext-real Element of REAL
L * N is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,L,N) is set
R is Element of the carrier of T
s1 is V11() real ext-real Element of REAL
N2 is V11() real ext-real set

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

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

(T,f,S) . n is Element of the carrier of T
((T,f,S) . n) - R is Element of the carrier of T
- R is Element of the carrier of T
K192(T,((T,f,S) . n),(- R)) is Element of the carrier of T
||.(((T,f,S) . n) - R).|| is V11() real ext-real Element of REAL
S . n is V11() real ext-real Element of REAL
(S . n) - L is V11() real ext-real Element of REAL
abs ((S . n) - L) is V11() real ext-real Element of REAL
((S . n) - L) * N is Element of the carrier of T
K249( the Mult of T,((S . n) - L),N) is set
||.(((S . n) - L) * N).|| is V11() real ext-real Element of REAL
* (abs ((S . n) - L)) is V11() real ext-real Element of REAL
* (s1 / ( + L)) is V11() real ext-real Element of REAL
f . n is Element of the carrier of T
(S . n) * (f . n) is Element of the carrier of T
K249( the Mult of T,(S . n),(f . n)) is set
((S . n) * (f . n)) - (L * N) is Element of the carrier of T
- (L * N) is Element of the carrier of T
K192(T,((S . n) * (f . n)),(- (L * N))) is Element of the carrier of T
||.(((S . n) * (f . n)) - (L * N)).|| is V11() real ext-real Element of REAL
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
((S . n) * (f . n)) - (0. T) is Element of the carrier of T
- (0. T) is Element of the carrier of T
K192(T,((S . n) * (f . n)),(- (0. T))) is Element of the carrier of T
(((S . n) * (f . n)) - (0. T)) - (L * N) is Element of the carrier of T
K192(T,(((S . n) * (f . n)) - (0. T)),(- (L * N))) is Element of the carrier of T
||.((((S . n) * (f . n)) - (0. T)) - (L * N)).|| is V11() real ext-real Element of REAL
(S . n) * N is Element of the carrier of T
K249( the Mult of T,(S . n),N) is set
((S . n) * N) - ((S . n) * N) is Element of the carrier of T
- ((S . n) * N) is Element of the carrier of T
K192(T,((S . n) * N),(- ((S . n) * N))) is Element of the carrier of T
((S . n) * (f . n)) - (((S . n) * N) - ((S . n) * N)) is Element of the carrier of T
- (((S . n) * N) - ((S . n) * N)) is Element of the carrier of T
K192(T,((S . n) * (f . n)),(- (((S . n) * N) - ((S . n) * N)))) is Element of the carrier of T
(((S . n) * (f . n)) - (((S . n) * N) - ((S . n) * N))) - (L * N) is Element of the carrier of T
K192(T,(((S . n) * (f . n)) - (((S . n) * N) - ((S . n) * N))),(- (L * N))) is Element of the carrier of T
||.((((S . n) * (f . n)) - (((S . n) * N) - ((S . n) * N))) - (L * N)).|| is V11() real ext-real Element of REAL
((S . n) * (f . n)) - ((S . n) * N) is Element of the carrier of T
K192(T,((S . n) * (f . n)),(- ((S . n) * N))) is Element of the carrier of T
(((S . n) * (f . n)) - ((S . n) * N)) + ((S . n) * N) is Element of the carrier of T
((((S . n) * (f . n)) - ((S . n) * N)) + ((S . n) * N)) - (L * N) is Element of the carrier of T
K192(T,((((S . n) * (f . n)) - ((S . n) * N)) + ((S . n) * N)),(- (L * N))) is Element of the carrier of T
||.(((((S . n) * (f . n)) - ((S . n) * N)) + ((S . n) * N)) - (L * N)).|| is V11() real ext-real Element of REAL
(f . n) - N is Element of the carrier of T
- N is Element of the carrier of T
K192(T,(f . n),(- N)) is Element of the carrier of T
(S . n) * ((f . n) - N) is Element of the carrier of T
K249( the Mult of T,(S . n),((f . n) - N)) is set
((S . n) * ((f . n) - N)) + ((S . n) * N) is Element of the carrier of T
(((S . n) * ((f . n) - N)) + ((S . n) * N)) - (L * N) is Element of the carrier of T
K192(T,(((S . n) * ((f . n) - N)) + ((S . n) * N)),(- (L * N))) is Element of the carrier of T
||.((((S . n) * ((f . n) - N)) + ((S . n) * N)) - (L * N)).|| is V11() real ext-real Element of REAL
((S . n) * N) - (L * N) is Element of the carrier of T
K192(T,((S . n) * N),(- (L * N))) is Element of the carrier of T
((S . n) * ((f . n) - N)) + (((S . n) * N) - (L * N)) is Element of the carrier of T
||.(((S . n) * ((f . n) - N)) + (((S . n) * N) - (L * N))).|| is V11() real ext-real Element of REAL
((S . n) * ((f . n) - N)) + (((S . n) - L) * N) is Element of the carrier of T
||.(((S . n) * ((f . n) - N)) + (((S . n) - L) * N)).|| is V11() real ext-real Element of REAL
||.((S . n) * ((f . n) - N)).|| is V11() real ext-real Element of REAL
||.((S . n) * ((f . n) - N)).|| + ||.(((S . n) - L) * N).|| is V11() real ext-real Element of REAL
||.((f . n) - N).|| is V11() real ext-real Element of REAL
abs (S . n) is V11() real ext-real Element of REAL
L * (s1 / ( + L)) is V11() real ext-real Element of REAL
(abs (S . n)) * ||.((f . n) - N).|| is V11() real ext-real Element of REAL
(L * (s1 / ( + L))) + ( * (s1 / ( + L))) is V11() real ext-real Element of REAL
(s1 / ( + L)) * ( + L) is V11() real ext-real Element of REAL

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

f is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(T,f,S) is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
lim (T,f,S) is Element of the carrier of T
lim f is Element of the carrier of T
(lim S) * (lim f) is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(lim S),(lim f)) is set
N is V11() real ext-real Element of REAL
N * (lim f) is Element of the carrier of T
K249( the Mult of T,N,(lim f)) is set
R is V11() real ext-real set
||.(lim f).|| is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
||.(lim f).|| + s1 is V11() real ext-real Element of REAL

N2 is V11() real ext-real Element of REAL
N2 / (||.(lim f).|| + s1) is V11() real ext-real Element of REAL

(T,f,S) . y is Element of the carrier of T
((T,f,S) . y) - (N * (lim f)) is Element of the carrier of T
- (N * (lim f)) is Element of the carrier of T
K192(T,((T,f,S) . y),(- (N * (lim f)))) is Element of the carrier of T
||.(((T,f,S) . y) - (N * (lim f))).|| is V11() real ext-real Element of REAL
S . y is V11() real ext-real Element of REAL
(S . y) - N is V11() real ext-real Element of REAL
abs ((S . y) - N) is V11() real ext-real Element of REAL
((S . y) - N) * (lim f) is Element of the carrier of T
K249( the Mult of T,((S . y) - N),(lim f)) is set
||.(((S . y) - N) * (lim f)).|| is V11() real ext-real Element of REAL
||.(lim f).|| * (abs ((S . y) - N)) is V11() real ext-real Element of REAL
||.(lim f).|| * (N2 / (||.(lim f).|| + s1)) is V11() real ext-real Element of REAL
abs (S . y) is V11() real ext-real Element of REAL
f . y is Element of the carrier of T
(f . y) - (lim f) is Element of the carrier of T
- (lim f) is Element of the carrier of T
K192(T,(f . y),(- (lim f))) is Element of the carrier of T
||.((f . y) - (lim f)).|| is V11() real ext-real Element of REAL
(S . y) * (f . y) is Element of the carrier of T
K249( the Mult of T,(S . y),(f . y)) is set
((S . y) * (f . y)) - (N * (lim f)) is Element of the carrier of T
K192(T,((S . y) * (f . y)),(- (N * (lim f)))) is Element of the carrier of T
||.(((S . y) * (f . y)) - (N * (lim f))).|| is V11() real ext-real Element of REAL
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
((S . y) * (f . y)) - (0. T) is Element of the carrier of T
- (0. T) is Element of the carrier of T
K192(T,((S . y) * (f . y)),(- (0. T))) is Element of the carrier of T
(((S . y) * (f . y)) - (0. T)) - (N * (lim f)) is Element of the carrier of T
K192(T,(((S . y) * (f . y)) - (0. T)),(- (N * (lim f)))) is Element of the carrier of T
||.((((S . y) * (f . y)) - (0. T)) - (N * (lim f))).|| is V11() real ext-real Element of REAL
(S . y) * (lim f) is Element of the carrier of T
K249( the Mult of T,(S . y),(lim f)) is set
((S . y) * (lim f)) - ((S . y) * (lim f)) is Element of the carrier of T
- ((S . y) * (lim f)) is Element of the carrier of T
K192(T,((S . y) * (lim f)),(- ((S . y) * (lim f)))) is Element of the carrier of T
((S . y) * (f . y)) - (((S . y) * (lim f)) - ((S . y) * (lim f))) is Element of the carrier of T
- (((S . y) * (lim f)) - ((S . y) * (lim f))) is Element of the carrier of T
K192(T,((S . y) * (f . y)),(- (((S . y) * (lim f)) - ((S . y) * (lim f))))) is Element of the carrier of T
(((S . y) * (f . y)) - (((S . y) * (lim f)) - ((S . y) * (lim f)))) - (N * (lim f)) is Element of the carrier of T
K192(T,(((S . y) * (f . y)) - (((S . y) * (lim f)) - ((S . y) * (lim f)))),(- (N * (lim f)))) is Element of the carrier of T
||.((((S . y) * (f . y)) - (((S . y) * (lim f)) - ((S . y) * (lim f)))) - (N * (lim f))).|| is V11() real ext-real Element of REAL
((S . y) * (f . y)) - ((S . y) * (lim f)) is Element of the carrier of T
K192(T,((S . y) * (f . y)),(- ((S . y) * (lim f)))) is Element of the carrier of T
(((S . y) * (f . y)) - ((S . y) * (lim f))) + ((S . y) * (lim f)) is Element of the carrier of T
((((S . y) * (f . y)) - ((S . y) * (lim f))) + ((S . y) * (lim f))) - (N * (lim f)) is Element of the carrier of T
K192(T,((((S . y) * (f . y)) - ((S . y) * (lim f))) + ((S . y) * (lim f))),(- (N * (lim f)))) is Element of the carrier of T
||.(((((S . y) * (f . y)) - ((S . y) * (lim f))) + ((S . y) * (lim f))) - (N * (lim f))).|| is V11() real ext-real Element of REAL
(S . y) * ((f . y) - (lim f)) is Element of the carrier of T
K249( the Mult of T,(S . y),((f . y) - (lim f))) is set
((S . y) * ((f . y) - (lim f))) + ((S . y) * (lim f)) is Element of the carrier of T
(((S . y) * ((f . y) - (lim f))) + ((S . y) * (lim f))) - (N * (lim f)) is Element of the carrier of T
K192(T,(((S . y) * ((f . y) - (lim f))) + ((S . y) * (lim f))),(- (N * (lim f)))) is Element of the carrier of T
||.((((S . y) * ((f . y) - (lim f))) + ((S . y) * (lim f))) - (N * (lim f))).|| is V11() real ext-real Element of REAL
((S . y) * (lim f)) - (N * (lim f)) is Element of the carrier of T
K192(T,((S . y) * (lim f)),(- (N * (lim f)))) is Element of the carrier of T
((S . y) * ((f . y) - (lim f))) + (((S . y) * (lim f)) - (N * (lim f))) is Element of the carrier of T
||.(((S . y) * ((f . y) - (lim f))) + (((S . y) * (lim f)) - (N * (lim f)))).|| is V11() real ext-real Element of REAL
((S . y) * ((f . y) - (lim f))) + (((S . y) - N) * (lim f)) is Element of the carrier of T
||.(((S . y) * ((f . y) - (lim f))) + (((S . y) - N) * (lim f))).|| is V11() real ext-real Element of REAL
||.((S . y) * ((f . y) - (lim f))).|| is V11() real ext-real Element of REAL
||.((S . y) * ((f . y) - (lim f))).|| + ||.(((S . y) - N) * (lim f)).|| is V11() real ext-real Element of REAL
s1 * (N2 / (||.(lim f).|| + s1)) is V11() real ext-real Element of REAL
(abs (S . y)) * ||.((f . y) - (lim f)).|| is V11() real ext-real Element of REAL
(s1 * (N2 / (||.(lim f).|| + s1))) + (||.(lim f).|| * (N2 / (||.(lim f).|| + s1))) is V11() real ext-real Element of REAL
(N2 / (||.(lim f).|| + s1)) * (||.(lim f).|| + s1) is V11() real ext-real Element of REAL

the carrier of S is V1() set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
f ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of f
x0 is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
f + x0 is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f + x0) ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of f + x0
x0 ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of x0
(f ^\ T) + (x0 ^\ T) is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))

((f + x0) ^\ T) . N is Element of the carrier of S

(f + x0) . (N + T) is Element of the carrier of S
f . (N + T) is Element of the carrier of S
x0 . (N + T) is Element of the carrier of S
(f . (N + T)) + (x0 . (N + T)) is Element of the carrier of S
(f ^\ T) . N is Element of the carrier of S
((f ^\ T) . N) + (x0 . (N + T)) is Element of the carrier of S
(x0 ^\ T) . N is Element of the carrier of S
((f ^\ T) . N) + ((x0 ^\ T) . N) is Element of the carrier of S
((f ^\ T) + (x0 ^\ T)) . N is Element of the carrier of S

the carrier of S is V1() set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
f ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of f
x0 is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
f - x0 is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f - x0) ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of f - x0
x0 ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of x0
(f ^\ T) - (x0 ^\ T) is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))

((f - x0) ^\ T) . N is Element of the carrier of S

(f - x0) . (N + T) is Element of the carrier of S
f . (N + T) is Element of the carrier of S
x0 . (N + T) is Element of the carrier of S
(f . (N + T)) - (x0 . (N + T)) is Element of the carrier of S
- (x0 . (N + T)) is Element of the carrier of S
K192(S,(f . (N + T)),(- (x0 . (N + T)))) is Element of the carrier of S
(f ^\ T) . N is Element of the carrier of S
((f ^\ T) . N) - (x0 . (N + T)) is Element of the carrier of S
K192(S,((f ^\ T) . N),(- (x0 . (N + T)))) is Element of the carrier of S
(x0 ^\ T) . N is Element of the carrier of S
((f ^\ T) . N) - ((x0 ^\ T) . N) is Element of the carrier of S
- ((x0 ^\ T) . N) is Element of the carrier of S
K192(S,((f ^\ T) . N),(- ((x0 ^\ T) . N))) is Element of the carrier of S
((f ^\ T) - (x0 ^\ T)) . N is Element of the carrier of S

the carrier of S is V1() set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
f ^\ T is V1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of f

(f ^\ T) . x0 is Element of the carrier of S

f . (x0 + T) is Element of the carrier of S
0. S is V68(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S

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

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
lim S is Element of the carrier of T
f is Element of the carrier of T
N is V11() real ext-real Element of REAL

S . R is Element of the carrier of T

S . x0 is Element of the carrier of T
(S . R) - (S . x0) is Element of the carrier of T
- (S . x0) is Element of the carrier of T
K192(T,(S . R),(- (S . x0))) is Element of the carrier of T
||.((S . R) - (S . x0)).|| is V11() real ext-real Element of REAL
f - (S . x0) is Element of the carrier of T
K192(T,f,(- (S . x0))) is Element of the carrier of T
||.(f - (S . x0)).|| is V11() real ext-real Element of REAL
f - f is Element of the carrier of T
- f is Element of the carrier of T
K192(T,f,(- f)) is Element of the carrier of T
||.(f - f).|| is V11() real ext-real Element of REAL
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
||.(0. T).|| is V11() real ext-real Element of REAL

S . x0 is Element of the carrier of T

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
f is Element of the carrier of T
x0 is V11() real ext-real Element of REAL
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
N is V68(T) Element of the carrier of T
L is V11() real ext-real Element of REAL

+ 1 is V11() real ext-real Element of REAL
L / ( + 1) is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL

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

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

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

s1 + x0 is V11() real ext-real Element of REAL
(R ") + 0 is V11() real ext-real Element of REAL
1 / (R ") is V11() real ext-real Element of REAL
1 / (s1 + x0) is V11() real ext-real Element of REAL
(R ") " is V11() real ext-real Element of REAL
1 * ((R ") ") is V11() real ext-real Element of REAL

S . L is Element of the carrier of T
(S . L) - N is Element of the carrier of T
- N is Element of the carrier of T
K192(T,(S . L),(- N)) is Element of the carrier of T
||.((S . L) - N).|| is V11() real ext-real Element of REAL
N2 + x0 is V11() real ext-real Element of REAL
L + x0 is V11() real ext-real Element of REAL
1 / (L + x0) is V11() real ext-real Element of REAL
1 / (N2 + x0) is V11() real ext-real Element of REAL
(1 / (L + x0)) * is V11() real ext-real Element of REAL
(1 / (L + x0)) * f is Element of the carrier of T
the Mult of T is V16() V19(K7(REAL, the carrier of T)) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of T), the carrier of T))
K7(REAL, the carrier of T) is set
K7(K7(REAL, the carrier of T), the carrier of T) is set
K6(K7(K7(REAL, the carrier of T), the carrier of T)) is set
K249( the Mult of T,(1 / (L + x0)),f) is set
((1 / (L + x0)) * f) - (0. T) is Element of the carrier of T
- (0. T) is Element of the carrier of T
K192(T,((1 / (L + x0)) * f),(- (0. T))) is Element of the carrier of T
||.(((1 / (L + x0)) * f) - (0. T)).|| is V11() real ext-real Element of REAL
||.((1 / (L + x0)) * f).|| is V11() real ext-real Element of REAL
abs (1 / (L + x0)) is V11() real ext-real Element of REAL
(abs (1 / (L + x0))) * is V11() real ext-real Element of REAL

the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
0. T is V68(T) Element of the carrier of T
the ZeroF of T is Element of the carrier of T
S is V1() V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
lim S is Element of the carrier of T
f is Element of the carrier of T
x0 is V11() real ext-real Element of REAL

N is V11() real ext-real Element of REAL
+ 1 is V11() real ext-real Element of REAL
N / ( + 1) is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL

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

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

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

R + x0 is V11() real ext-real Element of REAL
(L ") + 0 is V11() real ext-real Element of REAL
1 / (L ") is V11() real ext-real Element of REAL
1 / (R + x0) is V11() real ext-real Element of REAL
(L ") " is V11() real ext-real Element of REAL
1 * ((L ") ") is V11() real ext-real Element of REAL