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