:: 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

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

{ b

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

{ b

min (N,L) is V11() real ext-real Element of REAL

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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