:: NDIFF_2 semantic presentation

REAL is non empty V49() V160() V161() V162() V166() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V49() V160() V166() set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() 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 non empty 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 L12()
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 non empty V49() V160() V161() V162() V163() V166() set
INT is non empty V49() V160() V161() V162() V163() V164() V166() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V132() V159() V160() V161() V162() V163() V164() V165() V166() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
S is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
T is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
R_VectorSpace_of_LinearOperators (S,T) is non empty V87() strict V112() V113() V114() V115() V116() V117() V118() L12()
the carrier of (R_VectorSpace_of_LinearOperators (S,T)) is non empty set
BoundedLinearOperators (S,T) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (S,T)))
K6( the carrier of (R_VectorSpace_of_LinearOperators (S,T))) is set
x0 is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
R_VectorSpace_of_LinearOperators (T,x0) is non empty V87() strict V112() V113() V114() V115() V116() V117() V118() L12()
the carrier of (R_VectorSpace_of_LinearOperators (T,x0)) is non empty set
BoundedLinearOperators (T,x0) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (T,x0)))
K6( the carrier of (R_VectorSpace_of_LinearOperators (T,x0))) is set
the carrier of S is non empty set
the carrier of T is non empty set
the carrier of x0 is non empty set
U is Element of BoundedLinearOperators (S,T)
modetrans (U,S,T) is non empty V16() V19( the carrier of S) V20( the carrier of T) Function-like total quasi_total V153(S,T) V154(S,T) Lipschitzian Element of K6(K7( the carrier of S, the carrier of T))
K7( the carrier of S, the carrier of T) is set
K6(K7( the carrier of S, the carrier of T)) is set
f1 is Element of BoundedLinearOperators (T,x0)
modetrans (f1,T,x0) is non empty V16() V19( the carrier of T) V20( the carrier of x0) Function-like total quasi_total V153(T,x0) V154(T,x0) Lipschitzian Element of K6(K7( the carrier of T, the carrier of x0))
K7( the carrier of T, the carrier of x0) is set
K6(K7( the carrier of T, the carrier of x0)) is set
(modetrans (f1,T,x0)) * (modetrans (U,S,T)) is non empty V16() V19( the carrier of S) V20( the carrier of x0) Function-like total quasi_total Element of K6(K7( the carrier of S, the carrier of x0))
K7( the carrier of S, the carrier of x0) is set
K6(K7( the carrier of S, the carrier of x0)) is set
R_VectorSpace_of_LinearOperators (S,x0) is non empty V87() strict V112() V113() V114() V115() V116() V117() V118() L12()
the carrier of (R_VectorSpace_of_LinearOperators (S,x0)) is non empty set
BoundedLinearOperators (S,x0) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (S,x0)))
K6( the carrier of (R_VectorSpace_of_LinearOperators (S,x0))) is set
S is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
T is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (S,T) is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (S,T)) is non empty set
x0 is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (T,x0) is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (T,x0)) is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
the carrier of x0 is non empty set
U is V16() Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (S,T))
modetrans (U,S,T) is non empty V16() V19( the carrier of S) V20( the carrier of T) Function-like total quasi_total V153(S,T) V154(S,T) Lipschitzian Element of K6(K7( the carrier of S, the carrier of T))
K7( the carrier of S, the carrier of T) is set
K6(K7( the carrier of S, the carrier of T)) is set
f1 is V16() Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (T,x0))
modetrans (f1,T,x0) is non empty V16() V19( the carrier of T) V20( the carrier of x0) Function-like total quasi_total V153(T,x0) V154(T,x0) Lipschitzian Element of K6(K7( the carrier of T, the carrier of x0))
K7( the carrier of T, the carrier of x0) is set
K6(K7( the carrier of T, the carrier of x0)) is set
(modetrans (f1,T,x0)) * (modetrans (U,S,T)) is non empty V16() V19( the carrier of S) V20( the carrier of x0) Function-like total quasi_total Element of K6(K7( the carrier of S, the carrier of x0))
K7( the carrier of S, the carrier of x0) is set
K6(K7( the carrier of S, the carrier of x0)) is set
R_NormSpace_of_BoundedLinearOperators (S,x0) is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (S,x0)) is non empty set
BoundedLinearOperators (S,x0) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (S,x0)))
R_VectorSpace_of_LinearOperators (S,x0) is non empty V87() strict V112() V113() V114() V115() V116() V117() V118() L12()
the carrier of (R_VectorSpace_of_LinearOperators (S,x0)) is non empty set
K6( the carrier of (R_VectorSpace_of_LinearOperators (S,x0))) is set
Zero_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0))) is Element of BoundedLinearOperators (S,x0)
Add_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0))) is V16() V19(K7((BoundedLinearOperators (S,x0)),(BoundedLinearOperators (S,x0)))) V20( BoundedLinearOperators (S,x0)) Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators (S,x0)),(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0))))
K7((BoundedLinearOperators (S,x0)),(BoundedLinearOperators (S,x0))) is set
K7(K7((BoundedLinearOperators (S,x0)),(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0))) is set
K6(K7(K7((BoundedLinearOperators (S,x0)),(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0)))) is set
Mult_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0))) is V16() V19(K7(REAL,(BoundedLinearOperators (S,x0)))) V20( BoundedLinearOperators (S,x0)) Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0))))
K7(REAL,(BoundedLinearOperators (S,x0))) is set
K7(K7(REAL,(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0))) is set
K6(K7(K7(REAL,(BoundedLinearOperators (S,x0))),(BoundedLinearOperators (S,x0)))) is set
BoundedLinearOperatorsNorm (S,x0) is non empty V16() V19( BoundedLinearOperators (S,x0)) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((BoundedLinearOperators (S,x0)),REAL))
K7((BoundedLinearOperators (S,x0)),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((BoundedLinearOperators (S,x0)),REAL)) is set
NORMSTR(# (BoundedLinearOperators (S,x0)),(Zero_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0)))),(Add_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0)))),(Mult_ ((BoundedLinearOperators (S,x0)),(R_VectorSpace_of_LinearOperators (S,x0)))),(BoundedLinearOperatorsNorm (S,x0)) #) is strict NORMSTR
S is non empty non trivial V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of S is non empty non trivial set
T is non empty non trivial V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of T is non empty non trivial set
K7( the carrier of T, the carrier of S) is set
K6(K7( the carrier of T, the carrier of S)) is set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
x0 is V16() V19( the carrier of T) V20( the carrier of S) Function-like Element of K6(K7( the carrier of T, the carrier of S))
dom x0 is Element of K6( the carrier of T)
K6( the carrier of T) is set
U is Element of the carrier of T
{U} is non empty set
diff (x0,U) is V16() Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (T,S))
R_NormSpace_of_BoundedLinearOperators (T,S) is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (T,S)) is non empty set
0. T is V68(T) Element of the carrier of T
0. S is V68(S) Element of the carrier of S
x0 /. U is Element of the carrier of S
f1 is Neighbourhood of U
N1 is V16() V19( the carrier of T) V20( the carrier of S) Function-like RestFunc-like Element of K6(K7( the carrier of T, the carrier of S))
N1 /. (0. T) is Element of the carrier of S
N1 is V16() V19( the carrier of T) V20( the carrier of S) Function-like RestFunc-like Element of K6(K7( the carrier of T, the carrier of S))
N1 /. (0. T) is Element of the carrier of S
R2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like constant total quasi_total Element of K6(K7(NAT, the carrier of T))
rng R2 is Element of K6( the carrier of T)
f2 is Element of the carrier of T
N2 is non empty V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
N2 * f2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
(N2 * f2) + R2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng ((N2 * f2) + R2) is Element of K6( the carrier of T)
N1 /* (N2 * f2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
abs N2 is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(abs N2) " is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((abs N2) ") (#) (N1 /* (N2 * f2)) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
lim (((abs N2) ") (#) (N1 /* (N2 * f2))) is Element of the carrier of S
L2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(((abs N2) ") (#) (N1 /* (N2 * f2))) . L2 is Element of the carrier of S
dom N1 is Element of K6( the carrier of T)
rng (N2 * f2) is Element of K6( the carrier of T)
(N1 /* (N2 * f2)) . L2 is Element of the carrier of S
((abs N2) ") . L2 is V11() real ext-real Element of REAL
(((abs N2) ") . L2) * ((N1 /* (N2 * f2)) . L2) is Element of the carrier of S
(abs N2) . L2 is V11() real ext-real Element of REAL
((abs N2) . L2) " is V11() real ext-real Element of REAL
(((abs N2) . L2) ") * ((N1 /* (N2 * f2)) . L2) is Element of the carrier of S
N2 . L2 is V11() real ext-real Element of REAL
abs (N2 . L2) is V11() real ext-real Element of REAL
(abs (N2 . L2)) " is V11() real ext-real Element of REAL
((abs (N2 . L2)) ") * ((N1 /* (N2 * f2)) . L2) is Element of the carrier of S
(N2 * f2) . L2 is Element of the carrier of T
N1 /. ((N2 * f2) . L2) is Element of the carrier of S
((abs (N2 . L2)) ") * (N1 /. ((N2 * f2) . L2)) is Element of the carrier of S
(N2 . L2) * (0. T) is Element of the carrier of T
N1 /. ((N2 . L2) * (0. T)) is Element of the carrier of S
((abs (N2 . L2)) ") * (N1 /. ((N2 . L2) * (0. T))) is Element of the carrier of S
((abs (N2 . L2)) ") * (N1 /. (0. T)) is Element of the carrier of S
(((abs N2) ") (#) (N1 /* (N2 * f2))) . 0 is Element of the carrier of S
dom N1 is Element of K6( the carrier of T)
L2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total non-zero 0. T -convergent Element of K6(K7(NAT, the carrier of T))
rng L2 is Element of K6( the carrier of T)
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N2 . L1 is V11() real ext-real Element of REAL
abs (N2 . L1) is V11() real ext-real Element of REAL
L2 . L1 is Element of the carrier of T
||.(L2 . L1).|| is V11() real ext-real Element of REAL
(N2 . L1) * f2 is Element of the carrier of T
||.((N2 . L1) * f2).|| is V11() real ext-real Element of REAL
||.f2.|| is V11() real ext-real Element of REAL
(abs (N2 . L1)) * ||.f2.|| is V11() real ext-real Element of REAL
(abs (N2 . L1)) " is V11() real ext-real Element of REAL
((abs (N2 . L1)) ") * ||.(L2 . L1).|| is V11() real ext-real Element of REAL
((abs (N2 . L1)) ") * (abs (N2 . L1)) is V11() real ext-real Element of REAL
(((abs (N2 . L1)) ") * (abs (N2 . L1))) * ||.f2.|| is V11() real ext-real Element of REAL
1 * ||.f2.|| is V11() real ext-real Element of REAL
||.(L2 . L1).|| " is V11() real ext-real Element of REAL
||.f2.|| * (||.(L2 . L1).|| ") is V11() real ext-real Element of REAL
||.(L2 . L1).|| * (||.(L2 . L1).|| ") is V11() real ext-real Element of REAL
((abs (N2 . L1)) ") * (||.(L2 . L1).|| * (||.(L2 . L1).|| ")) is V11() real ext-real Element of REAL
||.(L2 . L1).|| / ||.(L2 . L1).|| is V11() real ext-real Element of REAL
((abs (N2 . L1)) ") * (||.(L2 . L1).|| / ||.(L2 . L1).||) is V11() real ext-real Element of REAL
((abs (N2 . L1)) ") * 1 is V11() real ext-real Element of REAL
||.L2.|| is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.L2.|| . L1 is V11() real ext-real Element of REAL
(||.L2.|| . L1) " is V11() real ext-real Element of REAL
||.f2.|| * ((||.L2.|| . L1) ") is V11() real ext-real Element of REAL
rng (N2 * f2) is Element of K6( the carrier of T)
(((abs N2) ") (#) (N1 /* (N2 * f2))) . L1 is Element of the carrier of S
(N1 /* (N2 * f2)) . L1 is Element of the carrier of S
((abs N2) ") . L1 is V11() real ext-real Element of REAL
(((abs N2) ") . L1) * ((N1 /* (N2 * f2)) . L1) is Element of the carrier of S
(abs N2) . L1 is V11() real ext-real Element of REAL
((abs N2) . L1) " is V11() real ext-real Element of REAL
(((abs N2) . L1) ") * ((N1 /* (N2 * f2)) . L1) is Element of the carrier of S
((abs (N2 . L1)) ") * ((N1 /* (N2 * f2)) . L1) is Element of the carrier of S
(N2 * f2) . L1 is Element of the carrier of T
N1 /. ((N2 * f2) . L1) is Element of the carrier of S
((abs (N2 . L1)) ") * (N1 /. ((N2 * f2) . L1)) is Element of the carrier of S
N1 /. (L2 . L1) is Element of the carrier of S
||.L2.|| " is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(||.L2.|| ") . L1 is V11() real ext-real Element of REAL
||.f2.|| * ((||.L2.|| ") . L1) is V11() real ext-real Element of REAL
(||.f2.|| * ((||.L2.|| ") . L1)) * (N1 /. (L2 . L1)) is Element of the carrier of S
((||.L2.|| ") . L1) * (N1 /. (L2 . L1)) is Element of the carrier of S
||.f2.|| * (((||.L2.|| ") . L1) * (N1 /. (L2 . L1))) is Element of the carrier of S
N1 /* L2 is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(N1 /* L2) . L1 is Element of the carrier of S
((||.L2.|| ") . L1) * ((N1 /* L2) . L1) is Element of the carrier of S
||.f2.|| * (((||.L2.|| ") . L1) * ((N1 /* L2) . L1)) is Element of the carrier of S
(||.L2.|| ") (#) (N1 /* L2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
((||.L2.|| ") (#) (N1 /* L2)) . L1 is Element of the carrier of S
||.f2.|| * (((||.L2.|| ") (#) (N1 /* L2)) . L1) is Element of the carrier of S
||.f2.|| * ((||.L2.|| ") (#) (N1 /* L2)) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(||.f2.|| * ((||.L2.|| ") (#) (N1 /* L2))) . L1 is Element of the carrier of S
lim ((||.L2.|| ") (#) (N1 /* L2)) is Element of the carrier of S
||.f2.|| * (0. S) is Element of the carrier of S
L2 is V11() real ext-real Element of REAL
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
LB1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N2 " is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(N2 ") (#) (N1 /* (N2 * f2)) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
((N2 ") (#) (N1 /* (N2 * f2))) . LB1 is Element of the carrier of S
(((N2 ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S) is Element of the carrier of S
- (0. S) is Element of the carrier of S
K192(S,(((N2 ") (#) (N1 /* (N2 * f2))) . LB1),(- (0. S))) is Element of the carrier of S
||.((((N2 ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S)).|| is V11() real ext-real Element of REAL
||.(((N2 ") (#) (N1 /* (N2 * f2))) . LB1).|| is V11() real ext-real Element of REAL
(N1 /* (N2 * f2)) . LB1 is Element of the carrier of S
(N2 ") . LB1 is V11() real ext-real Element of REAL
((N2 ") . LB1) * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.(((N2 ") . LB1) * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
N2 . LB1 is V11() real ext-real Element of REAL
(N2 . LB1) " is V11() real ext-real Element of REAL
((N2 . LB1) ") * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.(((N2 . LB1) ") * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
abs ((N2 . LB1) ") is V11() real ext-real Element of REAL
abs (abs ((N2 . LB1) ")) is V11() real ext-real Element of REAL
||.((N1 /* (N2 * f2)) . LB1).|| is V11() real ext-real Element of REAL
(abs (abs ((N2 . LB1) "))) * ||.((N1 /* (N2 * f2)) . LB1).|| is V11() real ext-real Element of REAL
(abs ((N2 . LB1) ")) * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.((abs ((N2 . LB1) ")) * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
abs ((N2 ") . LB1) is V11() real ext-real Element of REAL
(abs ((N2 ") . LB1)) * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.((abs ((N2 ") . LB1)) * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
abs (N2 ") is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(abs (N2 ")) . LB1 is V11() real ext-real Element of REAL
((abs (N2 ")) . LB1) * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.(((abs (N2 ")) . LB1) * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
((abs N2) ") . LB1 is V11() real ext-real Element of REAL
(((abs N2) ") . LB1) * ((N1 /* (N2 * f2)) . LB1) is Element of the carrier of S
||.((((abs N2) ") . LB1) * ((N1 /* (N2 * f2)) . LB1)).|| is V11() real ext-real Element of REAL
(((abs N2) ") (#) (N1 /* (N2 * f2))) . LB1 is Element of the carrier of S
||.((((abs N2) ") (#) (N1 /* (N2 * f2))) . LB1).|| is V11() real ext-real Element of REAL
((((abs N2) ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S) is Element of the carrier of S
K192(S,((((abs N2) ") (#) (N1 /* (N2 * f2))) . LB1),(- (0. S))) is Element of the carrier of S
||.(((((abs N2) ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S)).|| is V11() real ext-real Element of REAL
x0 /* ((N2 * f2) + R2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
x0 /* R2 is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(x0 /* ((N2 * f2) + R2)) - (x0 /* R2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(diff (x0,U)) . f2 is Element of the carrier of S
dom N1 is Element of K6( the carrier of T)
rng (N2 * f2) is Element of K6( the carrier of T)
BoundedLinearOperators (T,S) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (T,S)))
R_VectorSpace_of_LinearOperators (T,S) is non empty V87() strict V112() V113() V114() V115() V116() V117() V118() L12()
the carrier of (R_VectorSpace_of_LinearOperators (T,S)) is non empty set
K6( the carrier of (R_VectorSpace_of_LinearOperators (T,S))) is set
Zero_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S))) is Element of BoundedLinearOperators (T,S)
Add_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S))) is V16() V19(K7((BoundedLinearOperators (T,S)),(BoundedLinearOperators (T,S)))) V20( BoundedLinearOperators (T,S)) Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators (T,S)),(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S))))
K7((BoundedLinearOperators (T,S)),(BoundedLinearOperators (T,S))) is set
K7(K7((BoundedLinearOperators (T,S)),(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S))) is set
K6(K7(K7((BoundedLinearOperators (T,S)),(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S)))) is set
Mult_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S))) is V16() V19(K7(REAL,(BoundedLinearOperators (T,S)))) V20( BoundedLinearOperators (T,S)) Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S))))
K7(REAL,(BoundedLinearOperators (T,S))) is set
K7(K7(REAL,(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S))) is set
K6(K7(K7(REAL,(BoundedLinearOperators (T,S))),(BoundedLinearOperators (T,S)))) is set
BoundedLinearOperatorsNorm (T,S) is non empty V16() V19( BoundedLinearOperators (T,S)) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((BoundedLinearOperators (T,S)),REAL))
K7((BoundedLinearOperators (T,S)),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((BoundedLinearOperators (T,S)),REAL)) is set
NORMSTR(# (BoundedLinearOperators (T,S)),(Zero_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S)))),(Add_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S)))),(Mult_ ((BoundedLinearOperators (T,S)),(R_VectorSpace_of_LinearOperators (T,S)))),(BoundedLinearOperatorsNorm (T,S)) #) is strict NORMSTR
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . L1 is Element of the carrier of S
(((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . L1) - ((diff (x0,U)) . f2) is Element of the carrier of S
- ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . L1),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
||.((((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . L1) - ((diff (x0,U)) . f2)).|| is V11() real ext-real Element of REAL
((N2 ") (#) (N1 /* (N2 * f2))) . L1 is Element of the carrier of S
||.(((N2 ") (#) (N1 /* (N2 * f2))) . L1).|| is V11() real ext-real Element of REAL
N2 . L1 is V11() real ext-real Element of REAL
dom R2 is V160() V161() V162() V163() V164() V165() Element of K6(NAT)
R2 . L1 is Element of the carrier of T
dom ((N2 * f2) + R2) is V160() V161() V162() V163() V164() V165() Element of K6(NAT)
((N2 * f2) + R2) . L1 is Element of the carrier of T
(N2 * f2) . L1 is Element of the carrier of T
((N2 * f2) . L1) + (R2 . L1) is Element of the carrier of T
(N2 . L1) * f2 is Element of the carrier of T
((N2 . L1) * f2) + U is Element of the carrier of T
((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1 is Element of the carrier of S
(N2 ") . L1 is V11() real ext-real Element of REAL
((N2 ") . L1) * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1) is Element of the carrier of S
(((N2 ") . L1) * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1)) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 ") . L1) * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1)),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(N2 . L1) " is V11() real ext-real Element of REAL
((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1) is Element of the carrier of S
(((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1)) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) - (x0 /* R2)) . L1)),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(x0 /* ((N2 * f2) + R2)) . L1 is Element of the carrier of S
(x0 /* R2) . L1 is Element of the carrier of S
((x0 /* ((N2 * f2) + R2)) . L1) - ((x0 /* R2) . L1) is Element of the carrier of S
- ((x0 /* R2) . L1) is Element of the carrier of S
K192(S,((x0 /* ((N2 * f2) + R2)) . L1),(- ((x0 /* R2) . L1))) is Element of the carrier of S
((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) . L1) - ((x0 /* R2) . L1)) is Element of the carrier of S
(((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) . L1) - ((x0 /* R2) . L1))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((x0 /* ((N2 * f2) + R2)) . L1) - ((x0 /* R2) . L1))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
x0 /. (((N2 * f2) + R2) . L1) is Element of the carrier of S
(x0 /. (((N2 * f2) + R2) . L1)) - ((x0 /* R2) . L1) is Element of the carrier of S
K192(S,(x0 /. (((N2 * f2) + R2) . L1)),(- ((x0 /* R2) . L1))) is Element of the carrier of S
((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - ((x0 /* R2) . L1)) is Element of the carrier of S
(((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - ((x0 /* R2) . L1))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - ((x0 /* R2) . L1))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
x0 /. (R2 . L1) is Element of the carrier of S
(x0 /. (((N2 * f2) + R2) . L1)) - (x0 /. (R2 . L1)) is Element of the carrier of S
- (x0 /. (R2 . L1)) is Element of the carrier of S
K192(S,(x0 /. (((N2 * f2) + R2) . L1)),(- (x0 /. (R2 . L1)))) is Element of the carrier of S
((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - (x0 /. (R2 . L1))) is Element of the carrier of S
(((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - (x0 /. (R2 . L1)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * ((x0 /. (((N2 * f2) + R2) . L1)) - (x0 /. (R2 . L1)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
x0 /. (((N2 * f2) . L1) + (R2 . L1)) is Element of the carrier of S
(x0 /. (((N2 * f2) . L1) + (R2 . L1))) - (x0 /. (R2 . L1)) is Element of the carrier of S
K192(S,(x0 /. (((N2 * f2) . L1) + (R2 . L1))),(- (x0 /. (R2 . L1)))) is Element of the carrier of S
((N2 . L1) ") * ((x0 /. (((N2 * f2) . L1) + (R2 . L1))) - (x0 /. (R2 . L1))) is Element of the carrier of S
(((N2 . L1) ") * ((x0 /. (((N2 * f2) . L1) + (R2 . L1))) - (x0 /. (R2 . L1)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * ((x0 /. (((N2 * f2) . L1) + (R2 . L1))) - (x0 /. (R2 . L1)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
((N2 . L1) * f2) + (R2 . L1) is Element of the carrier of T
x0 /. (((N2 . L1) * f2) + (R2 . L1)) is Element of the carrier of S
(x0 /. (((N2 . L1) * f2) + (R2 . L1))) - (x0 /. (R2 . L1)) is Element of the carrier of S
K192(S,(x0 /. (((N2 . L1) * f2) + (R2 . L1))),(- (x0 /. (R2 . L1)))) is Element of the carrier of S
((N2 . L1) ") * ((x0 /. (((N2 . L1) * f2) + (R2 . L1))) - (x0 /. (R2 . L1))) is Element of the carrier of S
(((N2 . L1) ") * ((x0 /. (((N2 . L1) * f2) + (R2 . L1))) - (x0 /. (R2 . L1)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * ((x0 /. (((N2 . L1) * f2) + (R2 . L1))) - (x0 /. (R2 . L1)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(((N2 . L1) * f2) + U) - U is Element of the carrier of T
- U is Element of the carrier of T
K192(T,(((N2 . L1) * f2) + U),(- U)) is Element of the carrier of T
(diff (x0,U)) . ((((N2 . L1) * f2) + U) - U) is Element of the carrier of S
N1 /. ((((N2 . L1) * f2) + U) - U) is Element of the carrier of S
((diff (x0,U)) . ((((N2 . L1) * f2) + U) - U)) + (N1 /. ((((N2 . L1) * f2) + U) - U)) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . ((((N2 . L1) * f2) + U) - U)) + (N1 /. ((((N2 . L1) * f2) + U) - U))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . ((((N2 . L1) * f2) + U) - U)) + (N1 /. ((((N2 . L1) * f2) + U) - U)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . ((((N2 . L1) * f2) + U) - U)) + (N1 /. ((((N2 . L1) * f2) + U) - U)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
U - U is Element of the carrier of T
K192(T,U,(- U)) is Element of the carrier of T
((N2 . L1) * f2) + (U - U) is Element of the carrier of T
(diff (x0,U)) . (((N2 . L1) * f2) + (U - U)) is Element of the carrier of S
((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. ((((N2 . L1) * f2) + U) - U)) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. ((((N2 . L1) * f2) + U) - U))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. ((((N2 . L1) * f2) + U) - U)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. ((((N2 . L1) * f2) + U) - U)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
N1 /. (((N2 . L1) * f2) + (U - U)) is Element of the carrier of S
((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. (((N2 . L1) * f2) + (U - U))) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. (((N2 . L1) * f2) + (U - U)))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. (((N2 . L1) * f2) + (U - U))))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (U - U))) + (N1 /. (((N2 . L1) * f2) + (U - U))))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
((N2 . L1) * f2) + (0. T) is Element of the carrier of T
(diff (x0,U)) . (((N2 . L1) * f2) + (0. T)) is Element of the carrier of S
((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (U - U))) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (U - U)))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (U - U))))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (U - U))))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
N1 /. (((N2 . L1) * f2) + (0. T)) is Element of the carrier of S
((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (0. T))) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (0. T)))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (0. T))))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . (((N2 . L1) * f2) + (0. T))) + (N1 /. (((N2 . L1) * f2) + (0. T))))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(diff (x0,U)) . ((N2 . L1) * f2) is Element of the carrier of S
((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. (((N2 . L1) * f2) + (0. T))) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. (((N2 . L1) * f2) + (0. T)))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. (((N2 . L1) * f2) + (0. T))))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. (((N2 . L1) * f2) + (0. T))))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
N1 /. ((N2 . L1) * f2) is Element of the carrier of S
((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. ((N2 . L1) * f2)) is Element of the carrier of S
((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. ((N2 . L1) * f2))) is Element of the carrier of S
(((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. ((N2 . L1) * f2)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 . L1) ") * (((diff (x0,U)) . ((N2 . L1) * f2)) + (N1 /. ((N2 . L1) * f2)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
((N2 . L1) ") * (N1 /. ((N2 . L1) * f2)) is Element of the carrier of S
((N2 . L1) ") * ((diff (x0,U)) . ((N2 . L1) * f2)) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((diff (x0,U)) . ((N2 . L1) * f2))) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((diff (x0,U)) . ((N2 . L1) * f2)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((diff (x0,U)) . ((N2 . L1) * f2)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
L2 is Element of BoundedLinearOperators (T,S)
modetrans (L2,T,S) is non empty V16() V19( the carrier of T) V20( the carrier of S) Function-like total quasi_total V153(T,S) V154(T,S) Lipschitzian Element of K6(K7( the carrier of T, the carrier of S))
(modetrans (L2,T,S)) . ((N2 . L1) * f2) is Element of the carrier of S
((N2 . L1) ") * ((modetrans (L2,T,S)) . ((N2 . L1) * f2)) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((modetrans (L2,T,S)) . ((N2 . L1) * f2))) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((modetrans (L2,T,S)) . ((N2 . L1) * f2)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((modetrans (L2,T,S)) . ((N2 . L1) * f2)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(modetrans (L2,T,S)) . f2 is Element of the carrier of S
(N2 . L1) * ((modetrans (L2,T,S)) . f2) is Element of the carrier of S
((N2 . L1) ") * ((N2 . L1) * ((modetrans (L2,T,S)) . f2)) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * ((modetrans (L2,T,S)) . f2))) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * ((modetrans (L2,T,S)) . f2)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * ((modetrans (L2,T,S)) . f2)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
L2 . f2 is Element of the carrier of S
(N2 . L1) * (L2 . f2) is Element of the carrier of S
((N2 . L1) ") * ((N2 . L1) * (L2 . f2)) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * (L2 . f2))) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * (L2 . f2)))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((N2 . L1) ") * ((N2 . L1) * (L2 . f2)))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
((N2 . L1) ") * (N2 . L1) is V11() real ext-real Element of REAL
(((N2 . L1) ") * (N2 . L1)) * ((diff (x0,U)) . f2) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((((N2 . L1) ") * (N2 . L1)) * ((diff (x0,U)) . f2)) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((((N2 . L1) ") * (N2 . L1)) * ((diff (x0,U)) . f2))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((((N2 . L1) ") * (N2 . L1)) * ((diff (x0,U)) . f2))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
1 * ((diff (x0,U)) . f2) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (1 * ((diff (x0,U)) . f2)) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (1 * ((diff (x0,U)) . f2))) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (1 * ((diff (x0,U)) . f2))),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((diff (x0,U)) . f2) is Element of the carrier of S
((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((diff (x0,U)) . f2)) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + ((diff (x0,U)) . f2)),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
((diff (x0,U)) . f2) - ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,((diff (x0,U)) . f2),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (((diff (x0,U)) . f2) - ((diff (x0,U)) . f2)) is Element of the carrier of S
(((N2 . L1) ") * (N1 /. ((N2 . L1) * f2))) + (0. S) is Element of the carrier of S
((N2 ") . L1) * (N1 /. ((N2 . L1) * f2)) is Element of the carrier of S
N1 /. ((N2 * f2) . L1) is Element of the carrier of S
((N2 ") . L1) * (N1 /. ((N2 * f2) . L1)) is Element of the carrier of S
(N1 /* (N2 * f2)) . L1 is Element of the carrier of S
((N2 ") . L1) * ((N1 /* (N2 * f2)) . L1) is Element of the carrier of S
L2 is V11() real ext-real Element of REAL
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
LB1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((N2 ") (#) (N1 /* (N2 * f2))) . LB1 is Element of the carrier of S
(((N2 ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S) is Element of the carrier of S
K192(S,(((N2 ") (#) (N1 /* (N2 * f2))) . LB1),(- (0. S))) is Element of the carrier of S
||.((((N2 ") (#) (N1 /* (N2 * f2))) . LB1) - (0. S)).|| is V11() real ext-real Element of REAL
||.(((N2 ") (#) (N1 /* (N2 * f2))) . LB1).|| is V11() real ext-real Element of REAL
((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . LB1 is Element of the carrier of S
(((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . LB1) - ((diff (x0,U)) . f2) is Element of the carrier of S
- ((diff (x0,U)) . f2) is Element of the carrier of S
K192(S,(((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . LB1),(- ((diff (x0,U)) . f2))) is Element of the carrier of S
||.((((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) . LB1) - ((diff (x0,U)) . f2)).|| is V11() real ext-real Element of REAL
lim ((N2 ") (#) ((x0 /* ((N2 * f2) + R2)) - (x0 /* R2))) is Element of the carrier of S
S is non empty non trivial V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of S is non empty non trivial set
T is non empty non trivial V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of T is non empty non trivial set
K7( the carrier of T, the carrier of S) is set
K6(K7( the carrier of T, the carrier of S)) is set
K7(NAT, the carrier of T) is set
K6(K7(NAT, the carrier of T)) is set
x0 is V16() V19( the carrier of T) V20( the carrier of S) Function-like Element of K6(K7( the carrier of T, the carrier of S))
dom x0 is Element of K6( the carrier of T)
K6( the carrier of T) is set
U is Element of the carrier of T
{U} is non empty set
diff (x0,U) is V16() Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (T,S))
R_NormSpace_of_BoundedLinearOperators (T,S) is non empty V87() V112() V113() V114() V115() V116() V117() V118() V122() V123() RealNormSpace-like NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (T,S)) is non empty set
f1 is Neighbourhood of U
N1 is Element of the carrier of T
(diff (x0,U)) . N1 is Element of the carrier of S
f2 is non empty V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
f2 * N1 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
f2 " is non empty V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
N2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like constant total quasi_total Element of K6(K7(NAT, the carrier of T))
rng N2 is Element of K6( the carrier of T)
(f2 * N1) + N2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng ((f2 * N1) + N2) is Element of K6( the carrier of T)
x0 /* ((f2 * N1) + N2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
x0 /* N2 is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(x0 /* ((f2 * N1) + N2)) - (x0 /* N2) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2)) is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
lim ((f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2))) is Element of the carrier of S
R2 is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of T : not R2 <= ||.(b₁ - U).|| } is set
L2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N2 . L2 is Element of the carrier of T
L2 is V11() real ext-real Element of REAL
||.N1.|| is V11() real ext-real Element of REAL
||.N1.|| + 1 is V11() real ext-real Element of REAL
L2 / (||.N1.|| + 1) is V11() real ext-real Element of REAL
L1 is V11() real ext-real Element of REAL
L1 * ||.N1.|| is V11() real ext-real Element of REAL
||.N1.|| + 0 is V11() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V132() V159() V160() V161() V162() V163() V164() V165() V166() Element of NAT
L1 * (||.N1.|| + 1) is V11() real ext-real Element of REAL
L1 is V11() real ext-real Element of REAL
L1 * ||.N1.|| is V11() real ext-real Element of REAL
L1 is V11() real ext-real Element of REAL
L1 * ||.N1.|| is V11() real ext-real Element of REAL
lim f2 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() Element of REAL
LB1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
LB2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
R1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
f2 . R1 is V11() real ext-real Element of REAL
(f2 . R1) - 0 is V11() real ext-real Element of REAL
abs ((f2 . R1) - 0) is V11() real ext-real Element of REAL
(f2 * N1) . R1 is Element of the carrier of T
0. T is V68(T) Element of the carrier of T
((f2 * N1) . R1) - (0. T) is Element of the carrier of T
- (0. T) is Element of the carrier of T
K192(T,((f2 * N1) . R1),(- (0. T))) is Element of the carrier of T
||.(((f2 * N1) . R1) - (0. T)).|| is V11() real ext-real Element of REAL
(f2 . R1) * N1 is Element of the carrier of T
((f2 . R1) * N1) - (0. T) is Element of the carrier of T
K192(T,((f2 . R1) * N1),(- (0. T))) is Element of the carrier of T
||.(((f2 . R1) * N1) - (0. T)).|| is V11() real ext-real Element of REAL
||.((f2 . R1) * N1).|| is V11() real ext-real Element of REAL
abs (f2 . R1) is V11() real ext-real Element of REAL
(abs (f2 . R1)) * ||.N1.|| is V11() real ext-real Element of REAL
N2 . 0 is Element of the carrier of T
lim N2 is Element of the carrier of T
lim (f2 * N1) is Element of the carrier of T
lim ((f2 * N1) + N2) is Element of the carrier of T
(0. T) + U is Element of the carrier of T
L2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
f2 ^\ L2 is non empty V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of f2
(f2 ^\ L2) * N1 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
((f2 ^\ L2) * N1) + N2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng (((f2 ^\ L2) * N1) + N2) is Element of K6( the carrier of T)
L1 is set
LB1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(((f2 ^\ L2) * N1) + N2) . LB1 is Element of the carrier of T
L2 + LB1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((f2 * N1) + N2) . (L2 + LB1) is Element of the carrier of T
(((f2 * N1) + N2) . (L2 + LB1)) - U is Element of the carrier of T
- U is Element of the carrier of T
K192(T,(((f2 * N1) + N2) . (L2 + LB1)),(- U)) is Element of the carrier of T
||.((((f2 * N1) + N2) . (L2 + LB1)) - U).|| is V11() real ext-real Element of REAL
(f2 * N1) . (L2 + LB1) is Element of the carrier of T
N2 . (L2 + LB1) is Element of the carrier of T
((f2 * N1) . (L2 + LB1)) + (N2 . (L2 + LB1)) is Element of the carrier of T
(((f2 * N1) . (L2 + LB1)) + (N2 . (L2 + LB1))) - U is Element of the carrier of T
K192(T,(((f2 * N1) . (L2 + LB1)) + (N2 . (L2 + LB1))),(- U)) is Element of the carrier of T
||.((((f2 * N1) . (L2 + LB1)) + (N2 . (L2 + LB1))) - U).|| is V11() real ext-real Element of REAL
((f2 * N1) . (L2 + LB1)) + U is Element of the carrier of T
(((f2 * N1) . (L2 + LB1)) + U) - U is Element of the carrier of T
K192(T,(((f2 * N1) . (L2 + LB1)) + U),(- U)) is Element of the carrier of T
||.((((f2 * N1) . (L2 + LB1)) + U) - U).|| is V11() real ext-real Element of REAL
N2 . LB1 is Element of the carrier of T
((f2 * N1) . (L2 + LB1)) + (N2 . LB1) is Element of the carrier of T
(((f2 * N1) . (L2 + LB1)) + (N2 . LB1)) - U is Element of the carrier of T
K192(T,(((f2 * N1) . (L2 + LB1)) + (N2 . LB1)),(- U)) is Element of the carrier of T
||.((((f2 * N1) . (L2 + LB1)) + (N2 . LB1)) - U).|| is V11() real ext-real Element of REAL
f2 . (L2 + LB1) is V11() real ext-real Element of REAL
(f2 . (L2 + LB1)) * N1 is Element of the carrier of T
((f2 . (L2 + LB1)) * N1) + (N2 . LB1) is Element of the carrier of T
(((f2 . (L2 + LB1)) * N1) + (N2 . LB1)) - U is Element of the carrier of T
K192(T,(((f2 . (L2 + LB1)) * N1) + (N2 . LB1)),(- U)) is Element of the carrier of T
||.((((f2 . (L2 + LB1)) * N1) + (N2 . LB1)) - U).|| is V11() real ext-real Element of REAL
(f2 ^\ L2) . LB1 is V11() real ext-real Element of REAL
((f2 ^\ L2) . LB1) * N1 is Element of the carrier of T
(((f2 ^\ L2) . LB1) * N1) + (N2 . LB1) is Element of the carrier of T
((((f2 ^\ L2) . LB1) * N1) + (N2 . LB1)) - U is Element of the carrier of T
K192(T,((((f2 ^\ L2) . LB1) * N1) + (N2 . LB1)),(- U)) is Element of the carrier of T
||.(((((f2 ^\ L2) . LB1) * N1) + (N2 . LB1)) - U).|| is V11() real ext-real Element of REAL
((f2 ^\ L2) * N1) . LB1 is Element of the carrier of T
(((f2 ^\ L2) * N1) . LB1) + (N2 . LB1) is Element of the carrier of T
((((f2 ^\ L2) * N1) . LB1) + (N2 . LB1)) - U is Element of the carrier of T
K192(T,((((f2 ^\ L2) * N1) . LB1) + (N2 . LB1)),(- U)) is Element of the carrier of T
||.(((((f2 ^\ L2) * N1) . LB1) + (N2 . LB1)) - U).|| is V11() real ext-real Element of REAL
((((f2 ^\ L2) * N1) + N2) . LB1) - U is Element of the carrier of T
K192(T,((((f2 ^\ L2) * N1) + N2) . LB1),(- U)) is Element of the carrier of T
||.(((((f2 ^\ L2) * N1) + N2) . LB1) - U).|| is V11() real ext-real Element of REAL
LB2 is Element of the carrier of T
L2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
f2 ^\ L2 is non empty V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of f2
(f2 ^\ L2) * N1 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
((f2 ^\ L2) * N1) + N2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng (((f2 ^\ L2) * N1) + N2) is Element of K6( the carrier of T)
L2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
f2 ^\ L2 is non empty V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of f2
(f2 ^\ L2) * N1 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
((f2 ^\ L2) * N1) + N2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total Element of K6(K7(NAT, the carrier of T))
rng (((f2 ^\ L2) * N1) + N2) is Element of K6( the carrier of T)
((f2 * N1) + N2) ^\ L2 is non empty V16() V19( NAT ) V20( the carrier of T) Function-like total quasi_total subsequence of (f2 * N1) + N2
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(((f2 * N1) + N2) ^\ L2) . L1 is Element of the carrier of T
L2 + L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((f2 * N1) + N2) . (L2 + L1) is Element of the carrier of T
(f2 * N1) . (L2 + L1) is Element of the carrier of T
N2 . (L2 + L1) is Element of the carrier of T
((f2 * N1) . (L2 + L1)) + (N2 . (L2 + L1)) is Element of the carrier of T
((f2 * N1) . (L2 + L1)) + U is Element of the carrier of T
N2 . L1 is Element of the carrier of T
((f2 * N1) . (L2 + L1)) + (N2 . L1) is Element of the carrier of T
f2 . (L2 + L1) is V11() real ext-real Element of REAL
(f2 . (L2 + L1)) * N1 is Element of the carrier of T
((f2 . (L2 + L1)) * N1) + (N2 . L1) is Element of the carrier of T
(f2 ^\ L2) . L1 is V11() real ext-real Element of REAL
((f2 ^\ L2) . L1) * N1 is Element of the carrier of T
(((f2 ^\ L2) . L1) * N1) + (N2 . L1) is Element of the carrier of T
((f2 ^\ L2) * N1) . L1 is Element of the carrier of T
(((f2 ^\ L2) * N1) . L1) + (N2 . L1) is Element of the carrier of T
(((f2 ^\ L2) * N1) + N2) . L1 is Element of the carrier of T
(x0 /* ((f2 * N1) + N2)) ^\ L2 is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of x0 /* ((f2 * N1) + N2)
L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((x0 /* ((f2 * N1) + N2)) ^\ L2) . L1 is Element of the carrier of S
L2 + L1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(x0 /* ((f2 * N1) + N2)) . (L2 + L1) is Element of the carrier of S
((f2 * N1) + N2) . (L2 + L1) is Element of the carrier of T
x0 /. (((f2 * N1) + N2) . (L2 + L1)) is Element of the carrier of S
(((f2 * N1) + N2) ^\ L2) . L1 is Element of the carrier of T
x0 /. ((((f2 * N1) + N2) ^\ L2) . L1) is Element of the carrier of S
(((f2 ^\ L2) * N1) + N2) . L1 is Element of the carrier of T
x0 /. ((((f2 ^\ L2) * N1) + N2) . L1) is Element of the carrier of S
((f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2))) ^\ L2 is non empty V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total subsequence of (f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2))
(((f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2))) ^\ L2) . L1 is Element of the carrier of S
((f2 ") (#) ((x0 /* ((f2 * N1) + N2)) - (x0 /* N2))) . (L2 + L1) is Element of the carrier of S
((x0 /* ((f2 * N1) + N2)) - (x0 /* N2)) . (L2 + L1) is Element of the carrier of S
(f2 ") . (L2 + L1) is V11() real ext-real Element of REAL
((f2 ") . (L2 + L1)) * (((x0 /* ((f2 * N1) + N2)) - (x0 /* N2)) . (L2 + L1)) is Element of the carrier of S
f2 . (L2 + L1) is V11() real ext-real Element of REAL
(f2 . (L2 + L1)) " is V11() real ext-real Element of REAL
((f2 . (L2 + L1)) ") * (((x0 /* ((f2 * N1) + N2)) - (x0 /* N2)) . (L2 + L1)) is Element of the carrier of S
(f2 ^\ L2) . L1 is V11() real ext-real Element of REAL
((f2 ^\ L2) . L1) " is V11() real ext-real Element of REAL
(((f2 ^\ L2) . L1) ") * (((x0 /* ((f2 * N1) + N2)) - (x0 /* N2)) . (L2 + L1)) is Element of the carrier of S
(x0 /* N2) . (L2 + L1) is Element of the carrier of S
((x0 /* ((f2 * N1) + N2)) . (L2 + L1)) - ((x0 /* N2) . (L2 + L1)) is Element of the carrier of S
- ((x0 /* N2) . (L2 + L1)) is Element of the carrier of S
K192(S,((x0 /* ((f2 * N1) + N2)) . (L2 + L1)),(- ((x0 /* N2) . (L2 + L1)))) is Element of the carrier of S
(((f2 ^\ L2) . L1) ") * (((x0 /* ((f2 * N1) + N2)) . (L2 + L1)) - ((x0 /* N2) . (L2 + L1))) is Element of the carrier of S
(((x0 /* ((f2 * N1) + N2)) ^\ L2) . L1) - ((x0 /* N2) . (L2 + L1)) is Element of the carrier of S
K192(S,(((x0 /* ((f2 * N1) + N2)) ^\ L2) . L1),(- ((x0 /* N2) . (L2 + L1)))) is Element of the carrier of S
(((f2 ^\ L2) . L1) ") * ((((x0 /* ((f2 * N1) + N2)) ^\ L2) . L1) - ((x0 /* N2) . (L2 +