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
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
omega is V1() epsilon-transitive epsilon-connected ordinal V170() V171() V172() V173() V174() V175() V176() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
the_set_of_RealSequences is V1() set
K7(the_set_of_RealSequences,the_set_of_RealSequences) is set
K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences) is set
K6(K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences)) is set
K7(REAL,the_set_of_RealSequences) is set
K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences) is set
K6(K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences)) is set
Linear_Space_of_RealSequences is RLSStruct
the carrier of Linear_Space_of_RealSequences is set
K6( the carrier of Linear_Space_of_RealSequences) is set
the_set_of_l2RealSequences is Element of K6( the carrier of Linear_Space_of_RealSequences)
K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences) is set
K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL)) is set
RAT is V1() V49() V170() V171() V172() V173() V176() set
INT is V1() V49() V170() V171() V172() V173() V174() V176() set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
the V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V170() V171() V172() V173() V174() V175() V176() set is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V170() V171() V172() V173() V174() V175() V176() set
0c is set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
K39(0) is V11() real ext-real set
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
x0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
L + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
R + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
s1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of T is V1() set
K6( the carrier of T) is set
f is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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)
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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)
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S . f is Element of the carrier of T
f is set
S . f is set
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
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 V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
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))
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
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
f is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
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))
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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 V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f + x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
S is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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))
x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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 V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f - x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- x0 is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) x0 is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
f + (- x0) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued 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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(T,S,(f - x0)) . N is Element of the carrier of T
S . N is Element of the carrier of T
- x0 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
f + (- x0) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
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
||.N.|| is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL
||.N.|| + L is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
s1 / (||.N.|| + L) is V11() real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
R + x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
||.N.|| * (abs ((S . n) - L)) is V11() real ext-real Element of REAL
||.N.|| * (s1 / (||.N.|| + 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 / (||.N.|| + 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 / (||.N.|| + L))) + (||.N.|| * (s1 / (||.N.|| + L))) is V11() real ext-real Element of REAL
(s1 / (||.N.|| + L)) * (||.N.|| + L) is V11() real ext-real Element of REAL
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim S is V11() real ext-real Element of REAL
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
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
N2 is V11() real ext-real Element of REAL
N2 / (||.(lim f).|| + s1) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
L + R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
((f + x0) ^\ T) . N is Element of the carrier of S
N + T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
((f - x0) ^\ T) . N is Element of the carrier of S
N + T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(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
T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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 epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
(f ^\ T) . x0 is Element of the carrier of S
x0 + T is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of T is V1() set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S . R is Element of the carrier of T
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
S . x0 is Element of the carrier of T
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
||.f.|| is V11() real ext-real Element of REAL
||.f.|| + 1 is V11() real ext-real Element of REAL
L / (||.f.|| + 1) is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
R * ||.f.|| is V11() real ext-real Element of REAL
||.f.|| + 0 is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
R * (||.f.|| + 1) is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
R * ||.f.|| is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
R * ||.f.|| is V11() real ext-real Element of REAL
R " is V11() real ext-real Element of REAL
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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)) * ||.f.|| 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))) * ||.f.|| is V11() real ext-real Element of REAL
T is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
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
||.f.|| is V11() real ext-real Element of REAL
N is V11() real ext-real Element of REAL
||.f.|| + 1 is V11() real ext-real Element of REAL
N / (||.f.|| + 1) is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL
L * ||.f.|| is V11() real ext-real Element of REAL
||.f.|| + 0 is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
L * (||.f.|| + 1) is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL
L * ||.f.|| is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL
L * ||.f.|| 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 ext-real V129() V169() V170() V171() V172() V173() V174() V175() Element of NAT
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
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real