REAL is non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below Element of K10(REAL)
K10(REAL) is set
ExtREAL is non empty ext-real-membered V93() set
K11(NAT,ExtREAL) is V79() set
K10(K11(NAT,ExtREAL)) is set
K10(ExtREAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below set
K10(omega) is set
K10(NAT) is set
K11(NAT,REAL) is V78() V79() V80() set
K10(K11(NAT,REAL)) is set
COMPLEX is non empty V28() complex-membered V77() set
RAT is non empty V28() complex-membered ext-real-membered real-membered rational-membered V77() set
INT is non empty V28() complex-membered ext-real-membered real-membered rational-membered integer-membered V77() set
K11(COMPLEX,COMPLEX) is V78() set
K10(K11(COMPLEX,COMPLEX)) is set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is V78() set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is set
K11(REAL,REAL) is V78() V79() V80() set
K10(K11(REAL,REAL)) is set
K11(K11(REAL,REAL),REAL) is V78() V79() V80() set
K10(K11(K11(REAL,REAL),REAL)) is set
K11(RAT,RAT) is V8( RAT ) V78() V79() V80() set
K10(K11(RAT,RAT)) is set
K11(K11(RAT,RAT),RAT) is V8( RAT ) V78() V79() V80() set
K10(K11(K11(RAT,RAT),RAT)) is set
K11(INT,INT) is V8( RAT ) V8( INT ) V78() V79() V80() set
K10(K11(INT,INT)) is set
K11(K11(INT,INT),INT) is V8( RAT ) V8( INT ) V78() V79() V80() set
K10(K11(K11(INT,INT),INT)) is set
K11(NAT,NAT) is V8( RAT ) V8( INT ) V78() V79() V80() V81() set
K11(K11(NAT,NAT),NAT) is V8( RAT ) V8( INT ) V78() V79() V80() V81() set
K10(K11(K11(NAT,NAT),NAT)) is set
I[01] is non empty strict TopSpace-like real-membered TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() Element of NAT
K11(1,1) is V8( RAT ) V8( INT ) V78() V79() V80() V81() set
K10(K11(1,1)) is set
K11(K11(1,1),1) is V8( RAT ) V8( INT ) V78() V79() V80() V81() set
K10(K11(K11(1,1),1)) is set
K11(K11(1,1),REAL) is V78() V79() V80() set
K10(K11(K11(1,1),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() Element of NAT
K11(2,2) is V8( RAT ) V8( INT ) V78() V79() V80() V81() set
K11(K11(2,2),REAL) is V78() V79() V80() set
K10(K11(K11(2,2),REAL)) is set
RealSpace is non empty strict Reflexive discerning V211() triangle Discerning real-membered MetrStruct
real_dist is V4() V7(K11(REAL,REAL)) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(K11(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
R^1 is non empty strict TopSpace-like real-membered TopStruct
{} is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() set
the empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() set is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() set
0 is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() V121() Element of NAT
DYADIC is complex-membered ext-real-membered real-membered Element of K10(REAL)
[.0,1.] is complex-membered ext-real-membered real-membered V93() set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
K238(0,1) is complex-membered ext-real-membered real-membered V93() Element of K10(REAL)
K511(RealSpace) is TopStruct
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
K10( the carrier of R^1) is set
Closed-Interval-TSpace (0,1) is non empty strict real-membered SubSpace of R^1
the carrier of RealSpace is non empty complex-membered ext-real-membered real-membered set
I[01] is non empty strict TopSpace-like real-membered SubSpace of R^1
D is real-membered SubSpace of R^1
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
K10( the carrier of I[01]) is set
D is complex-membered ext-real-membered real-membered Element of K10( the carrier of I[01])
Cl D is closed complex-membered ext-real-membered real-membered Element of K10( the carrier of I[01])
[#] I[01] is non empty non proper open complex-membered ext-real-membered real-membered dense non boundary Element of K10( the carrier of I[01])
E is complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
R^1 | E is strict real-membered SubSpace of R^1
the carrier of (R^1 | E) is complex-membered ext-real-membered real-membered set
K10( the carrier of (R^1 | E)) is set
F is complex-membered ext-real-membered real-membered Element of K10( the carrier of (R^1 | E))
Up F is complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
Cl (Up F) is closed complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
(Cl (Up F)) /\ E is complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
f is set
b is V66() real ext-real set
a is V66() real ext-real Element of the carrier of RealSpace
a - 0 is V66() real ext-real Element of REAL
K117(0) is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() set
K115(a,K117(0)) is V66() real ext-real set
a - b is V66() real ext-real Element of REAL
K117(b) is V66() real ext-real set
K115(a,K117(b)) is V66() real ext-real set
Ball (a,b) is complex-membered ext-real-membered real-membered Element of K10( the carrier of RealSpace)
K10( the carrier of RealSpace) is set
a + b is V66() real ext-real Element of REAL
].(a - b),(a + b).[ is complex-membered ext-real-membered real-membered non left_end non right_end V93() set
b - b is V66() real ext-real Element of REAL
K115(b,K117(b)) is V66() real ext-real set
t is V66() real ext-real Element of REAL
a + 0 is V66() real ext-real Element of REAL
a - a is V66() real ext-real Element of REAL
K117(a) is V66() real ext-real set
K115(a,K117(a)) is V66() real ext-real set
Cl DYADIC is complex-membered ext-real-membered real-membered Element of K10(REAL)
E is complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
Cl E is closed complex-membered ext-real-membered real-membered Element of K10( the carrier of R^1)
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
F + F is Element of the carrier of E
2 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,F) is set
1 * F is Element of the carrier of E
K471( the Mult of E,1,F) is set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() Element of NAT
(1 + 1) * F is Element of the carrier of E
K471( the Mult of E,(1 + 1),F) is set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
f is Element of the carrier of E
F + f is Element of the carrier of E
(F + f) - f is Element of the carrier of E
- f is Element of the carrier of E
(F + f) + (- f) is Element of the carrier of E
f - f is Element of the carrier of E
f + (- f) is Element of the carrier of E
F + (f - f) is Element of the carrier of E
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
F + (0. E) is Element of the carrier of E
E is complex-membered ext-real-membered real-membered bounded_above set
F is V66() real ext-real non negative set
F ** E is complex-membered ext-real-membered real-membered set
F ** E is ext-real-membered set
E is complex-membered ext-real-membered real-membered bounded_above set
F is V66() real ext-real non positive set
F ** E is complex-membered ext-real-membered real-membered set
F ** E is ext-real-membered set
E is complex-membered ext-real-membered real-membered bounded_below set
F is V66() real ext-real non negative set
F ** E is complex-membered ext-real-membered real-membered set
F ** E is ext-real-membered set
E is non empty complex-membered ext-real-membered real-membered bounded_below set
F is V66() real ext-real non positive set
F ** E is non empty complex-membered ext-real-membered real-membered set
F ** E is non empty ext-real-membered set
E is V66() real ext-real set
{E} is non empty complex-membered ext-real-membered real-membered set
NAT --> E is non empty V4() V7( NAT ) V8({E}) Function-like constant total quasi_total V78() V79() V80() Element of K10(K11(NAT,{E}))
K11(NAT,{E}) is V78() V79() V80() set
K10(K11(NAT,{E})) is set
F is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
F + (NAT --> E) is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
E + F is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(F + (NAT --> E)) . f is V66() real ext-real set
(E + F) . f is V66() real ext-real set
(NAT --> E) . f is V66() real ext-real Element of REAL
(F + (NAT --> E)) . f is V66() real ext-real Element of REAL
F . f is V66() real ext-real Element of REAL
(F . f) + ((NAT --> E) . f) is V66() real ext-real Element of REAL
E + F is V4() V7( NAT ) Function-like total V78() V79() V80() set
(E + F) . f is V66() real ext-real Element of REAL
E is V66() real ext-real Element of REAL
NAT --> E is non empty V4() V7( NAT ) V8( REAL ) Function-like constant total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
lim (NAT --> E) is V66() real ext-real Element of REAL
(NAT --> E) . 0 is V66() real ext-real Element of REAL
E is V66() real ext-real set
F is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
E + F is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
lim (E + F) is V66() real ext-real Element of REAL
lim F is V66() real ext-real Element of REAL
E + (lim F) is V66() real ext-real Element of REAL
{E} is non empty complex-membered ext-real-membered real-membered set
NAT --> E is non empty V4() V7( NAT ) V8({E}) Function-like constant total quasi_total V78() V79() V80() Element of K10(K11(NAT,{E}))
K11(NAT,{E}) is V78() V79() V80() set
K10(K11(NAT,{E})) is set
F + (NAT --> E) is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
f is V66() real ext-real Element of REAL
NAT --> f is non empty V4() V7( NAT ) V8( REAL ) Function-like constant total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
lim (NAT --> f) is V66() real ext-real Element of REAL
(lim (NAT --> f)) + (lim F) is V66() real ext-real Element of REAL
E is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
F is V66() real ext-real set
F + E is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
f is V66() real ext-real Element of REAL
NAT --> f is non empty V4() V7( NAT ) V8( REAL ) Function-like constant total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
E + (NAT --> f) is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
a is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
NAT --> F is non empty V4() V7( NAT ) V8( the carrier of E) Function-like constant total quasi_total Element of K10(K11(NAT, the carrier of E))
K11(NAT, the carrier of E) is set
K10(K11(NAT, the carrier of E)) is set
f is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
f (#) (NAT --> F) is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
f * F is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
a is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(f (#) (NAT --> F)) . a is set
(f * F) . a is set
(NAT --> F) . a is Element of the carrier of E
(f (#) (NAT --> F)) . a is Element of the carrier of E
f . a is V66() real ext-real Element of REAL
(f . a) * ((NAT --> F) . a) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(f . a),((NAT --> F) . a)) is set
(f * F) . a is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
NAT --> F is non empty V4() V7( NAT ) V8( the carrier of E) Function-like constant total quasi_total Element of K10(K11(NAT, the carrier of E))
K11(NAT, the carrier of E) is set
K10(K11(NAT, the carrier of E)) is set
lim (NAT --> F) is Element of the carrier of E
(NAT --> F) . 0 is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
f is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
f * F is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
K11(NAT, the carrier of E) is set
K10(K11(NAT, the carrier of E)) is set
lim (f * F) is Element of the carrier of E
lim f is V66() real ext-real Element of REAL
(lim f) * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(lim f),F) is set
NAT --> F is non empty V4() V7( NAT ) V8( the carrier of E) Function-like constant total quasi_total Element of K10(K11(NAT, the carrier of E))
f (#) (NAT --> F) is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
lim (NAT --> F) is Element of the carrier of E
(lim f) * (lim (NAT --> F)) is Element of the carrier of E
K471( the Mult of E,(lim f),(lim (NAT --> F))) is set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
f is Element of the carrier of F
E is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() convergent Element of K10(K11(NAT,REAL))
E * f is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
K11(NAT, the carrier of F) is set
K10(K11(NAT, the carrier of F)) is set
NAT --> f is non empty V4() V7( NAT ) V8( the carrier of F) Function-like constant total quasi_total Element of K10(K11(NAT, the carrier of F))
E (#) (NAT --> f) is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
E is non empty NORMSTR
the carrier of E is non empty set
F is non empty NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
E is non empty RLSStruct
the carrier of E is non empty set
F is non empty RLSStruct
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
1 / 2 is V66() real ext-real non negative V121() Element of RAT
K118(2) is non empty V66() real ext-real positive non negative set
K116(1,K118(2)) is V66() real ext-real non negative set
E is non empty NORMSTR
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
F is Element of the carrier of E
(id E) . F is Element of the carrier of E
f is Element of the carrier of E
(id E) . f is Element of the carrier of E
((id E) . F) - ((id E) . f) is Element of the carrier of E
- ((id E) . f) is Element of the carrier of E
((id E) . F) + (- ((id E) . f)) is Element of the carrier of E
||.(((id E) . F) - ((id E) . f)).|| is V66() real ext-real Element of REAL
F - f is Element of the carrier of E
- f is Element of the carrier of E
F + (- f) is Element of the carrier of E
||.(F - f).|| is V66() real ext-real Element of REAL
E is non empty RLSStruct
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
F is Element of the carrier of E
f is Element of the carrier of E
F + f is Element of the carrier of E
(1 / 2) * (F + f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(F + f)) is set
(id E) . ((1 / 2) * (F + f)) is Element of the carrier of E
(id E) . F is Element of the carrier of E
(id E) . f is Element of the carrier of E
((id E) . F) + ((id E) . f) is Element of the carrier of E
(1 / 2) * (((id E) . F) + ((id E) . f)) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(((id E) . F) + ((id E) . f))) is set
F is Element of the carrier of E
f is Element of the carrier of E
(id E) . F is Element of the carrier of E
(id E) . f is Element of the carrier of E
a is V66() real ext-real set
1 - a is V66() real ext-real Element of REAL
K117(a) is V66() real ext-real set
K115(1,K117(a)) is V66() real ext-real set
(1 - a) * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - a),F) is set
a * f is Element of the carrier of E
K471( the Mult of E,a,f) is set
((1 - a) * F) + (a * f) is Element of the carrier of E
(id E) . (((1 - a) * F) + (a * f)) is Element of the carrier of E
(1 - a) * ((id E) . F) is Element of the carrier of E
K471( the Mult of E,(1 - a),((id E) . F)) is set
a * ((id E) . f) is Element of the carrier of E
K471( the Mult of E,a,((id E) . f)) is set
((1 - a) * ((id E) . F)) + (a * ((id E) . f)) is Element of the carrier of E
E is non empty NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K11( the carrier of F, the carrier of f) is set
K10(K11( the carrier of F, the carrier of f)) is set
a is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
b is non empty V4() V7( the carrier of F) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of f))
b * a is non empty V4() V7( the carrier of E) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of f))
K11( the carrier of E, the carrier of f) is set
K10(K11( the carrier of E, the carrier of f)) is set
s is Element of the carrier of E
(b * a) . s is Element of the carrier of f
stb is Element of the carrier of E
(b * a) . stb is Element of the carrier of f
((b * a) . s) - ((b * a) . stb) is Element of the carrier of f
- ((b * a) . stb) is Element of the carrier of f
((b * a) . s) + (- ((b * a) . stb)) is Element of the carrier of f
||.(((b * a) . s) - ((b * a) . stb)).|| is V66() real ext-real non negative Element of REAL
s - stb is Element of the carrier of E
- stb is Element of the carrier of E
s + (- stb) is Element of the carrier of E
||.(s - stb).|| is V66() real ext-real non negative Element of REAL
a . s is Element of the carrier of F
b . (a . s) is Element of the carrier of f
a . stb is Element of the carrier of F
b . (a . stb) is Element of the carrier of f
(a . s) - (a . stb) is Element of the carrier of F
- (a . stb) is Element of the carrier of F
(a . s) + (- (a . stb)) is Element of the carrier of F
||.((a . s) - (a . stb)).|| is V66() real ext-real non negative Element of REAL
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f * F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
rng f is Element of K10( the carrier of F)
K10( the carrier of F) is set
[#] F is non empty non proper Element of K10( the carrier of F)
(f /") /" is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f " is V4() Function-like set
(f /") " is V4() Function-like set
b is Element of the carrier of F
(f /") . b is Element of the carrier of E
f . ((f /") . b) is Element of the carrier of F
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
b is Element of the carrier of F
(f /") . b is Element of the carrier of E
t is Element of the carrier of F
(f /") . t is Element of the carrier of E
((f /") . b) - ((f /") . t) is Element of the carrier of E
- ((f /") . t) is Element of the carrier of E
((f /") . b) + (- ((f /") . t)) is Element of the carrier of E
||.(((f /") . b) - ((f /") . t)).|| is V66() real ext-real non negative Element of REAL
b - t is Element of the carrier of F
- t is Element of the carrier of F
b + (- t) is Element of the carrier of F
||.(b - t).|| is V66() real ext-real non negative Element of REAL
f . ((f /") . b) is Element of the carrier of F
f . ((f /") . t) is Element of the carrier of F
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
F /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K11( the carrier of F, the carrier of f) is set
K10(K11( the carrier of F, the carrier of f)) is set
a is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
b is non empty V4() V7( the carrier of F) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of f))
b * a is non empty V4() V7( the carrier of E) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of f))
K11( the carrier of E, the carrier of f) is set
K10(K11( the carrier of E, the carrier of f)) is set
s is Element of the carrier of E
(b * a) . s is Element of the carrier of f
stb is Element of the carrier of E
s + stb is Element of the carrier of E
(1 / 2) * (s + stb) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(s + stb)) is set
(b * a) . ((1 / 2) * (s + stb)) is Element of the carrier of f
(b * a) . stb is Element of the carrier of f
((b * a) . s) + ((b * a) . stb) is Element of the carrier of f
(1 / 2) * (((b * a) . s) + ((b * a) . stb)) is Element of the carrier of f
the Mult of f is V4() V7(K11(REAL, the carrier of f)) V8( the carrier of f) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of f), the carrier of f))
K11(REAL, the carrier of f) is set
K11(K11(REAL, the carrier of f), the carrier of f) is set
K10(K11(K11(REAL, the carrier of f), the carrier of f)) is set
K471( the Mult of f,(1 / 2),(((b * a) . s) + ((b * a) . stb))) is set
a . s is Element of the carrier of F
b . (a . s) is Element of the carrier of f
a . stb is Element of the carrier of F
b . (a . stb) is Element of the carrier of f
s + stb is Element of the carrier of E
(1 / 2) * (s + stb) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(s + stb)) is set
(b * a) . ((1 / 2) * (s + stb)) is Element of the carrier of f
a . ((1 / 2) * (s + stb)) is Element of the carrier of F
b . (a . ((1 / 2) * (s + stb))) is Element of the carrier of f
(a . s) + (a . stb) is Element of the carrier of F
(1 / 2) * ((a . s) + (a . stb)) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 / 2),((a . s) + (a . stb))) is set
b . ((1 / 2) * ((a . s) + (a . stb))) is Element of the carrier of f
((b * a) . s) + ((b * a) . stb) is Element of the carrier of f
(1 / 2) * (((b * a) . s) + ((b * a) . stb)) is Element of the carrier of f
K471( the Mult of f,(1 / 2),(((b * a) . s) + ((b * a) . stb))) is set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f * F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
rng f is Element of K10( the carrier of F)
K10( the carrier of F) is set
[#] F is non empty non proper Element of K10( the carrier of F)
dom f is Element of K10( the carrier of E)
K10( the carrier of E) is set
[#] E is non empty non proper Element of K10( the carrier of E)
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
(f /") * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
b is Element of the carrier of F
t is Element of the carrier of F
b + t is Element of the carrier of F
(1 / 2) * (b + t) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 / 2),(b + t)) is set
(f /") . ((1 / 2) * (b + t)) is Element of the carrier of E
(f /") . b is Element of the carrier of E
(f /") . t is Element of the carrier of E
((f /") . b) + ((f /") . t) is Element of the carrier of E
(1 / 2) * (((f /") . b) + ((f /") . t)) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(((f /") . b) + ((f /") . t))) is set
(f /") * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
f . ((f /") . b) is Element of the carrier of F
f . ((f /") . t) is Element of the carrier of F
b + t is Element of the carrier of F
(1 / 2) * (b + t) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(b + t)) is set
(f /") . ((1 / 2) * (b + t)) is Element of the carrier of E
((f /") . b) + ((f /") . t) is Element of the carrier of E
(1 / 2) * (((f /") . b) + ((f /") . t)) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(((f /") . b) + ((f /") . t))) is set
f . ((1 / 2) * (((f /") . b) + ((f /") . t))) is Element of the carrier of F
(f /") . (f . ((1 / 2) * (((f /") . b) + ((f /") . t)))) is Element of the carrier of E
((f /") * f) . ((1 / 2) * (((f /") . b) + ((f /") . t))) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
F /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K11( the carrier of F, the carrier of f) is set
K10(K11( the carrier of F, the carrier of f)) is set
a is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
b is non empty V4() V7( the carrier of F) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of f))
b * a is non empty V4() V7( the carrier of E) V8( the carrier of f) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of f))
K11( the carrier of E, the carrier of f) is set
K10(K11( the carrier of E, the carrier of f)) is set
s is Element of the carrier of E
(b * a) . s is Element of the carrier of f
stb is Element of the carrier of E
(b * a) . stb is Element of the carrier of f
1t is V66() real ext-real set
1 - 1t is V66() real ext-real Element of REAL
K117(1t) is V66() real ext-real set
K115(1,K117(1t)) is V66() real ext-real set
(1 - 1t) * s is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - 1t),s) is set
1t * stb is Element of the carrier of E
K471( the Mult of E,1t,stb) is set
((1 - 1t) * s) + (1t * stb) is Element of the carrier of E
(b * a) . (((1 - 1t) * s) + (1t * stb)) is Element of the carrier of f
(1 - 1t) * ((b * a) . s) is Element of the carrier of f
the Mult of f is V4() V7(K11(REAL, the carrier of f)) V8( the carrier of f) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of f), the carrier of f))
K11(REAL, the carrier of f) is set
K11(K11(REAL, the carrier of f), the carrier of f) is set
K10(K11(K11(REAL, the carrier of f), the carrier of f)) is set
K471( the Mult of f,(1 - 1t),((b * a) . s)) is set
1t * ((b * a) . stb) is Element of the carrier of f
K471( the Mult of f,1t,((b * a) . stb)) is set
((1 - 1t) * ((b * a) . s)) + (1t * ((b * a) . stb)) is Element of the carrier of f
a . s is Element of the carrier of F
b . (a . s) is Element of the carrier of f
a . stb is Element of the carrier of F
b . (a . stb) is Element of the carrier of f
((1 - 1t) * s) + (1t * stb) is Element of the carrier of E
(b * a) . (((1 - 1t) * s) + (1t * stb)) is Element of the carrier of f
a . (((1 - 1t) * s) + (1t * stb)) is Element of the carrier of F
b . (a . (((1 - 1t) * s) + (1t * stb))) is Element of the carrier of f
(1 - 1t) * (a . s) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - 1t),(a . s)) is set
1t * (a . stb) is Element of the carrier of F
K471( the Mult of F,1t,(a . stb)) is set
((1 - 1t) * (a . s)) + (1t * (a . stb)) is Element of the carrier of F
b . (((1 - 1t) * (a . s)) + (1t * (a . stb))) is Element of the carrier of f
((1 - 1t) * ((b * a) . s)) + (1t * ((b * a) . stb)) is Element of the carrier of f
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
f * F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
b is Element of the carrier of F
t is Element of the carrier of F
(f /") . b is Element of the carrier of E
(f /") . t is Element of the carrier of E
s is V66() real ext-real set
1 - s is V66() real ext-real Element of REAL
K117(s) is V66() real ext-real set
K115(1,K117(s)) is V66() real ext-real set
(1 - s) * b is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - s),b) is set
s * t is Element of the carrier of F
K471( the Mult of F,s,t) is set
((1 - s) * b) + (s * t) is Element of the carrier of F
(f /") . (((1 - s) * b) + (s * t)) is Element of the carrier of E
(1 - s) * ((f /") . b) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - s),((f /") . b)) is set
s * ((f /") . t) is Element of the carrier of E
K471( the Mult of E,s,((f /") . t)) is set
((1 - s) * ((f /") . b)) + (s * ((f /") . t)) is Element of the carrier of E
(f /") * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
f . ((f /") . b) is Element of the carrier of F
f . ((f /") . t) is Element of the carrier of F
((1 - s) * b) + (s * t) is Element of the carrier of F
(f /") . (((1 - s) * b) + (s * t)) is Element of the carrier of E
((1 - s) * ((f /") . b)) + (s * ((f /") . t)) is Element of the carrier of E
f . (((1 - s) * ((f /") . b)) + (s * ((f /") . t))) is Element of the carrier of F
(f /") . (f . (((1 - s) * ((f /") . b)) + (s * ((f /") . t)))) is Element of the carrier of E
((f /") * f) . (((1 - s) * ((f /") . b)) + (s * ((f /") . t))) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
F /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
E is non empty RLSStruct
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F is Element of the carrier of E
2 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,F) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
b is Element of the carrier of E
f . b is set
a . b is set
f . b is Element of the carrier of E
(2 * F) - b is Element of the carrier of E
- b is Element of the carrier of E
(2 * F) + (- b) is Element of the carrier of E
a . b is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,F) * (E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
a is Element of the carrier of E
((E,F) * (E,F)) . a is set
(id E) . a is set
((E,F) * (E,F)) . a is Element of the carrier of E
(E,F) . a is Element of the carrier of E
(E,F) . ((E,F) . a) is Element of the carrier of E
2 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,F) is set
(2 * F) - ((E,F) . a) is Element of the carrier of E
- ((E,F) . a) is Element of the carrier of E
(2 * F) + (- ((E,F) . a)) is Element of the carrier of E
(2 * F) - a is Element of the carrier of E
- a is Element of the carrier of E
(2 * F) + (- a) is Element of the carrier of E
(2 * F) - ((2 * F) - a) is Element of the carrier of E
- ((2 * F) - a) is Element of the carrier of E
(2 * F) + (- ((2 * F) - a)) is Element of the carrier of E
(2 * F) - (2 * F) is Element of the carrier of E
- (2 * F) is Element of the carrier of E
(2 * F) + (- (2 * F)) is Element of the carrier of E
((2 * F) - (2 * F)) + a is Element of the carrier of E
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
(0. E) + a is Element of the carrier of E
(id E) . a is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
(E,F) * (E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
(E,F) . F is Element of the carrier of E
2 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,F) is set
(2 * F) - F is Element of the carrier of E
- F is Element of the carrier of E
(2 * F) + (- F) is Element of the carrier of E
F + F is Element of the carrier of E
(F + F) - F is Element of the carrier of E
(F + F) + (- F) is Element of the carrier of E
F - F is Element of the carrier of E
F + (- F) is Element of the carrier of E
F + (F - F) is Element of the carrier of E
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
F + (0. E) is Element of the carrier of E
a is Element of the carrier of E
(E,F) . a is Element of the carrier of E
((E,F) . a) + a is Element of the carrier of E
2 * a is Element of the carrier of E
K471( the Mult of E,2,a) is set
(2 * F) - a is Element of the carrier of E
- a is Element of the carrier of E
(2 * F) + (- a) is Element of the carrier of E
a - a is Element of the carrier of E
a + (- a) is Element of the carrier of E
(2 * F) - (a - a) is Element of the carrier of E
- (a - a) is Element of the carrier of E
(2 * F) + (- (a - a)) is Element of the carrier of E
(2 * F) - (0. E) is Element of the carrier of E
- (0. E) is Element of the carrier of E
(2 * F) + (- (0. E)) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
f is Element of the carrier of E
(E,F) . f is Element of the carrier of E
((E,F) . f) - F is Element of the carrier of E
- F is Element of the carrier of E
((E,F) . f) + (- F) is Element of the carrier of E
F - f is Element of the carrier of E
- f is Element of the carrier of E
F + (- f) is Element of the carrier of E
1 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,1,F) is set
2 * F is Element of the carrier of E
K471( the Mult of E,2,F) is set
(2 * F) - f is Element of the carrier of E
(2 * F) + (- f) is Element of the carrier of E
(2 * F) - F is Element of the carrier of E
(2 * F) + (- F) is Element of the carrier of E
((2 * F) - F) - f is Element of the carrier of E
((2 * F) - F) + (- f) is Element of the carrier of E
2 - 1 is V66() real ext-real V120() V121() Element of INT
K117(1) is V66() real ext-real non positive V120() set
K115(2,K117(1)) is V66() real ext-real V120() set
(2 - 1) * F is Element of the carrier of E
K471( the Mult of E,(2 - 1),F) is set
((2 - 1) * F) - f is Element of the carrier of E
((2 - 1) * F) + (- f) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
f is Element of the carrier of E
(E,F) . f is Element of the carrier of E
((E,F) . f) - F is Element of the carrier of E
- F is Element of the carrier of E
((E,F) . f) + (- F) is Element of the carrier of E
||.(((E,F) . f) - F).|| is V66() real ext-real non negative Element of REAL
f - F is Element of the carrier of E
f + (- F) is Element of the carrier of E
||.(f - F).|| is V66() real ext-real non negative Element of REAL
F - f is Element of the carrier of E
- f is Element of the carrier of E
F + (- f) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
f is Element of the carrier of E
(E,F) . f is Element of the carrier of E
((E,F) . f) - f is Element of the carrier of E
- f is Element of the carrier of E
((E,F) . f) + (- f) is Element of the carrier of E
F - f is Element of the carrier of E
F + (- f) is Element of the carrier of E
2 * (F - f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,(F - f)) is set
2 * F is Element of the carrier of E
K471( the Mult of E,2,F) is set
(2 * F) - f is Element of the carrier of E
(2 * F) + (- f) is Element of the carrier of E
((2 * F) - f) - f is Element of the carrier of E
((2 * F) - f) + (- f) is Element of the carrier of E
f + f is Element of the carrier of E
(2 * F) - (f + f) is Element of the carrier of E
- (f + f) is Element of the carrier of E
(2 * F) + (- (f + f)) is Element of the carrier of E
2 * f is Element of the carrier of E
K471( the Mult of E,2,f) is set
(2 * F) - (2 * f) is Element of the carrier of E
- (2 * f) is Element of the carrier of E
(2 * F) + (- (2 * f)) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
f is Element of the carrier of E
(E,F) . f is Element of the carrier of E
((E,F) . f) - f is Element of the carrier of E
- f is Element of the carrier of E
((E,F) . f) + (- f) is Element of the carrier of E
||.(((E,F) . f) - f).|| is V66() real ext-real non negative Element of REAL
f - F is Element of the carrier of E
- F is Element of the carrier of E
f + (- F) is Element of the carrier of E
||.(f - F).|| is V66() real ext-real non negative Element of REAL
2 * ||.(f - F).|| is V66() real ext-real non negative Element of REAL
F - f is Element of the carrier of E
F + (- f) is Element of the carrier of E
2 * (F - f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,(F - f)) is set
abs 2 is V66() real ext-real V121() Element of REAL
||.(F - f).|| is V66() real ext-real non negative Element of REAL
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
(E,F) /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
rng (E,F) is Element of K10( the carrier of E)
K10( the carrier of E) is set
[#] E is non empty non proper Element of K10( the carrier of E)
(E,F) " is V4() Function-like one-to-one set
(E,F) * (E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
(E,F) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
a is Element of the carrier of E
(E,F) . a is Element of the carrier of E
b is Element of the carrier of E
(E,F) . b is Element of the carrier of E
((E,F) . a) - ((E,F) . b) is Element of the carrier of E
- ((E,F) . b) is Element of the carrier of E
((E,F) . a) + (- ((E,F) . b)) is Element of the carrier of E
||.(((E,F) . a) - ((E,F) . b)).|| is V66() real ext-real non negative Element of REAL
a - b is Element of the carrier of E
- b is Element of the carrier of E
a + (- b) is Element of the carrier of E
||.(a - b).|| is V66() real ext-real non negative Element of REAL
2 * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,2,F) is set
(2 * F) - a is Element of the carrier of E
- a is Element of the carrier of E
(2 * F) + (- a) is Element of the carrier of E
(2 * F) - b is Element of the carrier of E
(2 * F) + (- b) is Element of the carrier of E
((2 * F) - a) - (2 * F) is Element of the carrier of E
- (2 * F) is Element of the carrier of E
((2 * F) - a) + (- (2 * F)) is Element of the carrier of E
(((2 * F) - a) - (2 * F)) + b is Element of the carrier of E
(2 * F) - (2 * F) is Element of the carrier of E
(2 * F) + (- (2 * F)) is Element of the carrier of E
((2 * F) - (2 * F)) - a is Element of the carrier of E
((2 * F) - (2 * F)) + (- a) is Element of the carrier of E
(((2 * F) - (2 * F)) - a) + b is Element of the carrier of E
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
(0. E) - a is Element of the carrier of E
(0. E) + (- a) is Element of the carrier of E
((0. E) - a) + b is Element of the carrier of E
b - a is Element of the carrier of E
b + (- a) is Element of the carrier of E
{ b1 where b1 is non empty V4() V7( the carrier of a1) V8( the carrier of a1) Function-like total quasi_total Element of K10(K11( the carrier of a1, the carrier of a1)) : ( b1 is bijective & b1 is (a1,a1) & b1 . a2 = a2 & b1 . a3 = a3 ) } is set
{ ||.((b1 . ((1 / 2) * (a2 + a3))) - ((1 / 2) * (a2 + a3))).|| where b1 is non empty V4() V7( the carrier of a1) V8( the carrier of a1) Function-like total quasi_total Element of K10(K11( the carrier of a1, the carrier of a1)) : b1 in H1(a1,a2,a3) } is set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
a is complex-membered ext-real-membered real-membered set
F is Element of the carrier of E
f is Element of the carrier of E
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F + f is Element of the carrier of E
(1 / 2) * (F + f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(F + f)) is set
{ b1 where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : ( b1 is bijective & b1 is (E,E) & b1 . F = F & b1 . f = f ) } is set
{ ||.((b1 . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : b1 in H1(E,F,f) } is set
F - ((1 / 2) * (F + f)) is Element of the carrier of E
- ((1 / 2) * (F + f)) is Element of the carrier of E
F + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.(F - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
2 * ||.(F - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
t is ext-real set
s is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
s . ((1 / 2) * (F + f)) is Element of the carrier of E
(s . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
(s . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((s . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
stb is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
stb . F is Element of the carrier of E
stb . f is Element of the carrier of E
stb . ((1 / 2) * (F + f)) is Element of the carrier of E
(stb . ((1 / 2) * (F + f))) - F is Element of the carrier of E
- F is Element of the carrier of E
(stb . ((1 / 2) * (F + f))) + (- F) is Element of the carrier of E
||.((stb . ((1 / 2) * (F + f))) - F).|| is V66() real ext-real non negative Element of REAL
((1 / 2) * (F + f)) - F is Element of the carrier of E
((1 / 2) * (F + f)) + (- F) is Element of the carrier of E
||.(((1 / 2) * (F + f)) - F).|| is V66() real ext-real non negative Element of REAL
(stb . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
(stb . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((stb . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
||.((stb . ((1 / 2) * (F + f))) - F).|| + ||.(F - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
F is Element of the carrier of E
f is Element of the carrier of E
{ b1 where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : ( b1 is bijective & b1 is (E,E) & b1 . F = F & b1 . f = f ) } is set
F + f is Element of the carrier of E
(1 / 2) * (F + f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(F + f)) is set
(E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
a /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,((1 / 2) * (F + f))) * (a /") is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (F + f))) * (a /")) * (E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(((E,((1 / 2) * (F + f))) * (a /")) * (E,((1 / 2) * (F + f)))) * a is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
stb is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
stb . F is Element of the carrier of E
stb . f is Element of the carrier of E
stb /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
stb " is V4() Function-like set
2 * ((1 / 2) * (F + f)) is Element of the carrier of E
K471( the Mult of E,2,((1 / 2) * (F + f))) is set
2 * (1 / 2) is V66() real ext-real non negative V121() Element of RAT
(2 * (1 / 2)) * (F + f) is Element of the carrier of E
K471( the Mult of E,(2 * (1 / 2)),(F + f)) is set
(2 * ((1 / 2) * (F + f))) - F is Element of the carrier of E
- F is Element of the carrier of E
(2 * ((1 / 2) * (F + f))) + (- F) is Element of the carrier of E
(2 * ((1 / 2) * (F + f))) - f is Element of the carrier of E
- f is Element of the carrier of E
(2 * ((1 / 2) * (F + f))) + (- f) is Element of the carrier of E
dom stb is Element of K10( the carrier of E)
K10( the carrier of E) is set
[#] E is non empty non proper Element of K10( the carrier of E)
(stb /") . f is Element of the carrier of E
(stb /") . F is Element of the carrier of E
((((E,((1 / 2) * (F + f))) * (a /")) * (E,((1 / 2) * (F + f)))) * a) . F is Element of the carrier of E
(E,((1 / 2) * (F + f))) * (stb /") is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (F + f))) * (stb /")) * (E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(((E,((1 / 2) * (F + f))) * (stb /")) * (E,((1 / 2) * (F + f)))) . F is Element of the carrier of E
(E,((1 / 2) * (F + f))) . F is Element of the carrier of E
((E,((1 / 2) * (F + f))) * (stb /")) . ((E,((1 / 2) * (F + f))) . F) is Element of the carrier of E
((E,((1 / 2) * (F + f))) * (stb /")) . f is Element of the carrier of E
(E,((1 / 2) * (F + f))) . ((stb /") . f) is Element of the carrier of E
((((E,((1 / 2) * (F + f))) * (a /")) * (E,((1 / 2) * (F + f)))) * a) . f is Element of the carrier of E
(((E,((1 / 2) * (F + f))) * (stb /")) * (E,((1 / 2) * (F + f)))) . f is Element of the carrier of E
(E,((1 / 2) * (F + f))) . f is Element of the carrier of E
((E,((1 / 2) * (F + f))) * (stb /")) . ((E,((1 / 2) * (F + f))) . f) is Element of the carrier of E
((E,((1 / 2) * (F + f))) * (stb /")) . F is Element of the carrier of E
(E,((1 / 2) * (F + f))) . ((stb /") . F) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
a is non empty complex-membered ext-real-membered real-membered bounded_above Element of K10(REAL)
F is Element of the carrier of E
f is Element of the carrier of E
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F + f is Element of the carrier of E
(1 / 2) * (F + f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(F + f)) is set
{ b1 where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : ( b1 is bijective & b1 is (E,E) & b1 . F = F & b1 . f = f ) } is set
{ ||.((b1 . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : b1 in H1(E,F,f) } is set
sup a is V66() real ext-real set
2 ** a is non empty complex-membered ext-real-membered real-membered bounded_above set
2 ** a is non empty ext-real-membered set
(E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
s is ext-real set
stb is ext-real Element of ExtREAL
2 * stb is ext-real set
1t is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
1t . ((1 / 2) * (F + f)) is Element of the carrier of E
(1t . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
- ((1 / 2) * (F + f)) is Element of the carrier of E
(1t . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((1t . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
s1ta is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
s1ta . F is Element of the carrier of E
s1ta . f is Element of the carrier of E
(E,((1 / 2) * (F + f))) * s1ta is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
s1ta /" is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(s1ta /") * ((E,((1 / 2) * (F + f))) * s1ta) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,((1 / 2) * (F + f))) * ((s1ta /") * ((E,((1 / 2) * (F + f))) * s1ta)) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,((1 / 2) * (F + f))) * (s1ta /") is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (F + f))) * (s1ta /")) * ((E,((1 / 2) * (F + f))) * s1ta) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f)))) * s1ta is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
s1ta . ((1 / 2) * (F + f)) is Element of the carrier of E
(E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f))) is Element of the carrier of E
(s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))) is Element of the carrier of E
(E,((1 / 2) * (F + f))) . ((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f))))) is Element of the carrier of E
((E,((1 / 2) * (F + f))) * s1ta) . ((1 / 2) * (F + f)) is Element of the carrier of E
(s1ta /") . (((E,((1 / 2) * (F + f))) * s1ta) . ((1 / 2) * (F + f))) is Element of the carrier of E
(E,((1 / 2) * (F + f))) . ((s1ta /") . (((E,((1 / 2) * (F + f))) * s1ta) . ((1 / 2) * (F + f)))) is Element of the carrier of E
((s1ta /") * ((E,((1 / 2) * (F + f))) * s1ta)) . ((1 / 2) * (F + f)) is Element of the carrier of E
(E,((1 / 2) * (F + f))) . (((s1ta /") * ((E,((1 / 2) * (F + f))) * s1ta)) . ((1 / 2) * (F + f))) is Element of the carrier of E
((E,((1 / 2) * (F + f))) * ((s1ta /") * ((E,((1 / 2) * (F + f))) * s1ta))) . ((1 / 2) * (F + f)) is Element of the carrier of E
s1ta " is V4() Function-like set
((((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f)))) * s1ta) . ((1 / 2) * (F + f)) is Element of the carrier of E
(((((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f)))) * s1ta) . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
(((((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f)))) * s1ta) . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((((((E,((1 / 2) * (F + f))) * (s1ta /")) * (E,((1 / 2) * (F + f)))) * s1ta) . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
(s1ta . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
(s1ta . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((s1ta . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
s1 is ext-real Element of ExtREAL
s1 * ||.((s1ta . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is ext-real set
2 * ||.((s1ta . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
(s1ta /") . (s1ta . ((1 / 2) * (F + f))) is Element of the carrier of E
((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))) - (s1ta . ((1 / 2) * (F + f))) is Element of the carrier of E
- (s1ta . ((1 / 2) * (F + f))) is Element of the carrier of E
((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))) + (- (s1ta . ((1 / 2) * (F + f)))) is Element of the carrier of E
||.(((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))) - (s1ta . ((1 / 2) * (F + f)))).|| is V66() real ext-real non negative Element of REAL
((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f))))) - ((s1ta /") . (s1ta . ((1 / 2) * (F + f)))) is Element of the carrier of E
- ((s1ta /") . (s1ta . ((1 / 2) * (F + f)))) is Element of the carrier of E
((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f))))) + (- ((s1ta /") . (s1ta . ((1 / 2) * (F + f))))) is Element of the carrier of E
||.(((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f))))) - ((s1ta /") . (s1ta . ((1 / 2) * (F + f))))).|| is V66() real ext-real non negative Element of REAL
((E,((1 / 2) * (F + f))) . ((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))))) - ((1 / 2) * (F + f)) is Element of the carrier of E
((E,((1 / 2) * (F + f))) . ((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.(((E,((1 / 2) * (F + f))) . ((s1ta /") . ((E,((1 / 2) * (F + f))) . (s1ta . ((1 / 2) * (F + f)))))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
a is complex-membered ext-real-membered real-membered set
F is Element of the carrier of E
f is Element of the carrier of E
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
F + f is Element of the carrier of E
(1 / 2) * (F + f) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(F + f)) is set
{ b1 where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : ( b1 is bijective & b1 is (E,E) & b1 . F = F & b1 . f = f ) } is set
{ ||.((b1 . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : b1 in H1(E,F,f) } is set
b is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,((1 / 2) * (F + f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
stb is set
1t is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
1t . ((1 / 2) * (F + f)) is Element of the carrier of E
(1t . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
- ((1 / 2) * (F + f)) is Element of the carrier of E
(1t . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((1t . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
(id E) . F is Element of the carrier of E
(id E) . f is Element of the carrier of E
(id E) . ((1 / 2) * (F + f)) is Element of the carrier of E
((id E) . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
- ((1 / 2) * (F + f)) is Element of the carrier of E
((id E) . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.(((id E) . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
F - ((1 / 2) * (F + f)) is Element of the carrier of E
F + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.(F - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
2 * ||.(F - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
stb is non empty complex-membered ext-real-membered real-membered bounded_above Element of K10(REAL)
sup stb is V66() real ext-real set
s1ta is ext-real Element of ExtREAL
s1ta * (sup stb) is ext-real set
2 ** stb is non empty complex-membered ext-real-membered real-membered bounded_above set
2 ** stb is non empty ext-real-membered set
sup (2 ** stb) is V66() real ext-real set
b . ((1 / 2) * (F + f)) is Element of the carrier of E
(b . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f)) is Element of the carrier of E
(b . ((1 / 2) * (F + f))) + (- ((1 / 2) * (F + f))) is Element of the carrier of E
||.((b . ((1 / 2) * (F + f))) - ((1 / 2) * (F + f))).|| is V66() real ext-real non negative Element of REAL
2 * (sup stb) is V66() real ext-real Element of REAL
(2 * (sup stb)) - (sup stb) is V66() real ext-real Element of REAL
K117((sup stb)) is V66() real ext-real set
K115((2 * (sup stb)),K117((sup stb))) is V66() real ext-real set
(sup stb) - (sup stb) is V66() real ext-real Element of REAL
K115((sup stb),K117((sup stb))) is V66() real ext-real set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
dom f is Element of K10( the carrier of E)
K10( the carrier of E) is set
K11(NAT, the carrier of E) is set
K10(K11(NAT, the carrier of E)) is set
b is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
rng b is Element of K10( the carrier of E)
lim b is Element of the carrier of E
f /* b is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
K11(NAT, the carrier of F) is set
K10(K11(NAT, the carrier of F)) is set
f /. (lim b) is Element of the carrier of F
f . (lim b) is Element of the carrier of F
lim (f /* b) is Element of the carrier of F
t is Element of the carrier of E
f . t is Element of the carrier of F
s is V66() real ext-real Element of REAL
stb is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
1t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(f /* b) . 1t is Element of the carrier of F
((f /* b) . 1t) - (f . t) is Element of the carrier of F
- (f . t) is Element of the carrier of F
((f /* b) . 1t) + (- (f . t)) is Element of the carrier of F
||.(((f /* b) . 1t) - (f . t)).|| is V66() real ext-real non negative Element of REAL
b . 1t is Element of the carrier of E
(b . 1t) - t is Element of the carrier of E
- t is Element of the carrier of E
(b . 1t) + (- t) is Element of the carrier of E
||.((b . 1t) - t).|| is V66() real ext-real non negative Element of REAL
f . (b . 1t) is Element of the carrier of F
(f . (b . 1t)) - (f . t) is Element of the carrier of F
(f . (b . 1t)) + (- (f . t)) is Element of the carrier of F
||.((f . (b . 1t)) - (f . t)).|| is V66() real ext-real non negative Element of REAL
f * b is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
s is V66() real ext-real Element of REAL
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is Element of the carrier of E
f is Element of the carrier of E
f - F is Element of the carrier of E
- F is Element of the carrier of E
f + (- F) is Element of the carrier of E
a is V66() real ext-real set
1 - a is V66() real ext-real Element of REAL
K117(a) is V66() real ext-real set
K115(1,K117(a)) is V66() real ext-real set
(1 - a) * F is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - a),F) is set
a * f is Element of the carrier of E
K471( the Mult of E,a,f) is set
((1 - a) * F) + (a * f) is Element of the carrier of E
a * (f - F) is Element of the carrier of E
K471( the Mult of E,a,(f - F)) is set
F + (a * (f - F)) is Element of the carrier of E
1 * F is Element of the carrier of E
K471( the Mult of E,1,F) is set
a * F is Element of the carrier of E
K471( the Mult of E,a,F) is set
(1 * F) - (a * F) is Element of the carrier of E
- (a * F) is Element of the carrier of E
(1 * F) + (- (a * F)) is Element of the carrier of E
((1 * F) - (a * F)) + (a * f) is Element of the carrier of E
F - (a * F) is Element of the carrier of E
F + (- (a * F)) is Element of the carrier of E
(F - (a * F)) + (a * f) is Element of the carrier of E
F + (a * f) is Element of the carrier of E
(F + (a * f)) - (a * F) is Element of the carrier of E
(F + (a * f)) + (- (a * F)) is Element of the carrier of E
(a * f) - (a * F) is Element of the carrier of E
(a * f) + (- (a * F)) is Element of the carrier of E
F + ((a * f) - (a * F)) is Element of the carrier of E
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
t + 1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 |^ (t + 1) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 |^ t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
(2 |^ t) - s is V66() real ext-real V120() V121() Element of INT
K117(s) is V66() real ext-real V120() set
K115((2 |^ t),K117(s)) is V66() real ext-real V120() set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
s1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
za is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s / (2 |^ (t + 1)) is V66() real ext-real Element of REAL
K118((2 |^ (t + 1))) is V66() real ext-real set
K116(s,K118((2 |^ (t + 1)))) is V66() real ext-real set
1 - (s / (2 |^ (t + 1))) is V66() real ext-real Element of REAL
K117((s / (2 |^ (t + 1)))) is V66() real ext-real set
K115(1,K117((s / (2 |^ (t + 1))))) is V66() real ext-real set
(1 - (s / (2 |^ (t + 1)))) - (1 / 2) is V66() real ext-real Element of REAL
K117((1 / 2)) is V66() real ext-real non positive set
K115((1 - (s / (2 |^ (t + 1)))),K117((1 / 2))) is V66() real ext-real set
2 * (2 |^ t) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
1 / (2 |^ t) is V66() real ext-real Element of REAL
K118((2 |^ t)) is V66() real ext-real set
K116(1,K118((2 |^ t))) is V66() real ext-real set
(1 / 2) * (1 / (2 |^ t)) is V66() real ext-real Element of REAL
1 / (2 * (2 |^ t)) is V66() real ext-real V121() Element of RAT
K118((2 * (2 |^ t))) is V66() real ext-real set
K116(1,K118((2 * (2 |^ t)))) is V66() real ext-real set
za / (2 |^ (t + 1)) is V66() real ext-real Element of REAL
K116(za,K118((2 |^ (t + 1)))) is V66() real ext-real set
1 * (2 |^ t) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(1 * (2 |^ t)) / (2 |^ (t + 1)) is V66() real ext-real V121() Element of RAT
K116((1 * (2 |^ t)),K118((2 |^ (t + 1)))) is V66() real ext-real set
((1 * (2 |^ t)) / (2 |^ (t + 1))) - (s / (2 |^ (t + 1))) is V66() real ext-real Element of REAL
K115(((1 * (2 |^ t)) / (2 |^ (t + 1))),K117((s / (2 |^ (t + 1))))) is V66() real ext-real set
(1 / 2) - (s / (2 |^ (t + 1))) is V66() real ext-real Element of REAL
K115((1 / 2),K117((s / (2 |^ (t + 1))))) is V66() real ext-real set
a is Element of the carrier of E
((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,((1 - (s / (2 |^ (t + 1)))) - (1 / 2)),a) is set
b is Element of the carrier of E
(s / (2 |^ (t + 1))) * b is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),b) is set
(((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
za * a is Element of the carrier of E
K471( the Mult of E,za,a) is set
1 / (2 |^ (t + 1)) is V66() real ext-real V121() Element of RAT
K116(1,K118((2 |^ (t + 1)))) is V66() real ext-real set
(1 / (2 |^ (t + 1))) * (za * a) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),(za * a)) is set
(1 / (2 |^ (t + 1))) * s is V66() real ext-real Element of REAL
((1 / (2 |^ (t + 1))) * s) * b is Element of the carrier of E
K471( the Mult of E,((1 / (2 |^ (t + 1))) * s),b) is set
((1 / (2 |^ (t + 1))) * (za * a)) + (((1 / (2 |^ (t + 1))) * s) * b) is Element of the carrier of E
s * b is Element of the carrier of E
K471( the Mult of E,s,b) is set
(1 / (2 |^ (t + 1))) * (s * b) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),(s * b)) is set
((1 / (2 |^ (t + 1))) * (za * a)) + ((1 / (2 |^ (t + 1))) * (s * b)) is Element of the carrier of E
(za * a) + (s * b) is Element of the carrier of E
(1 / (2 |^ (t + 1))) * ((za * a) + (s * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),((za * a) + (s * b))) is set
(1 / (2 |^ t)) * ((za * a) + (s * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ t)),((za * a) + (s * b))) is set
(1 / 2) * ((1 / (2 |^ t)) * ((za * a) + (s * b))) is Element of the carrier of E
K471( the Mult of E,(1 / 2),((1 / (2 |^ t)) * ((za * a) + (s * b)))) is set
b - a is Element of the carrier of E
- a is Element of the carrier of E
b + (- a) is Element of the carrier of E
(s / (2 |^ (t + 1))) * (b - a) is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),(b - a)) is set
a + ((s / (2 |^ (t + 1))) * (b - a)) is Element of the carrier of E
(s / (2 |^ (t + 1))) * a is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),a) is set
((s / (2 |^ (t + 1))) * b) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
- ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
((s / (2 |^ (t + 1))) * b) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a + (((s / (2 |^ (t + 1))) * b) - ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
(a + ((s / (2 |^ (t + 1))) * b)) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
(a + ((s / (2 |^ (t + 1))) * b)) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
a + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
(a - ((s / (2 |^ (t + 1))) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
1 * a is Element of the carrier of E
K471( the Mult of E,1,a) is set
(1 * a) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
(1 * a) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
((1 * a) - ((s / (2 |^ (t + 1))) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
(1 - (s / (2 |^ (t + 1)))) * a is Element of the carrier of E
K471( the Mult of E,(1 - (s / (2 |^ (t + 1)))),a) is set
((1 - (s / (2 |^ (t + 1)))) * a) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
((1 - (s / (2 |^ (t + 1)))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
(((1 - (s / (2 |^ (t + 1)))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) - (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
- (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
(((1 - (s / (2 |^ (t + 1)))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + (- (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) is Element of the carrier of E
((((1 - (s / (2 |^ (t + 1)))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) - (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
((1 - (s / (2 |^ (t + 1)))) * a) - (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
((1 - (s / (2 |^ (t + 1)))) * a) + (- (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) is Element of the carrier of E
(((1 - (s / (2 |^ (t + 1)))) * a) - (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
((((1 - (s / (2 |^ (t + 1)))) * a) - (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
(1 - (s / (2 |^ (t + 1)))) - ((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) is V66() real ext-real Element of REAL
K117(((1 - (s / (2 |^ (t + 1)))) - (1 / 2))) is V66() real ext-real set
K115((1 - (s / (2 |^ (t + 1)))),K117(((1 - (s / (2 |^ (t + 1)))) - (1 / 2)))) is V66() real ext-real set
((1 - (s / (2 |^ (t + 1)))) - ((1 - (s / (2 |^ (t + 1)))) - (1 / 2))) * a is Element of the carrier of E
K471( the Mult of E,((1 - (s / (2 |^ (t + 1)))) - ((1 - (s / (2 |^ (t + 1)))) - (1 / 2))),a) is set
(((1 - (s / (2 |^ (t + 1)))) - ((1 - (s / (2 |^ (t + 1)))) - (1 / 2))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) is Element of the carrier of E
((((1 - (s / (2 |^ (t + 1)))) - ((1 - (s / (2 |^ (t + 1)))) - (1 / 2))) * a) + (((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
(1 / 2) * a is Element of the carrier of E
K471( the Mult of E,(1 / 2),a) is set
((1 / 2) * a) + ((((1 - (s / (2 |^ (t + 1)))) - (1 / 2)) * a) + ((s / (2 |^ (t + 1))) * b)) is Element of the carrier of E
a + ((1 / (2 |^ t)) * ((za * a) + (s * b))) is Element of the carrier of E
(1 / 2) * (a + ((1 / (2 |^ t)) * ((za * a) + (s * b)))) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(a + ((1 / (2 |^ t)) * ((za * a) + (s * b))))) is set
f . (a + ((s / (2 |^ (t + 1))) * (b - a))) is Element of the carrier of F
f . a is Element of the carrier of F
f . ((1 / (2 |^ t)) * ((za * a) + (s * b))) is Element of the carrier of F
(f . a) + (f . ((1 / (2 |^ t)) * ((za * a) + (s * b)))) is Element of the carrier of F
(1 / 2) * ((f . a) + (f . ((1 / (2 |^ t)) * ((za * a) + (s * b))))) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 / 2),((f . a) + (f . ((1 / (2 |^ t)) * ((za * a) + (s * b)))))) is set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
t + 1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 |^ (t + 1) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 |^ t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
(2 |^ t) + s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
((2 |^ t) + s) - (2 |^ (t + 1)) is V66() real ext-real V120() V121() Element of INT
K117((2 |^ (t + 1))) is V66() real ext-real V120() set
K115(((2 |^ t) + s),K117((2 |^ (t + 1)))) is V66() real ext-real V120() set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
2 * (2 |^ t) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(2 |^ t) + (2 |^ t) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
za is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s / (2 |^ (t + 1)) is V66() real ext-real Element of REAL
K118((2 |^ (t + 1))) is V66() real ext-real set
K116(s,K118((2 |^ (t + 1)))) is V66() real ext-real set
(s / (2 |^ (t + 1))) - (1 / 2) is V66() real ext-real Element of REAL
K115((s / (2 |^ (t + 1))),K117((1 / 2))) is V66() real ext-real set
(2 |^ (t + 1)) / (2 |^ (t + 1)) is V66() real ext-real V121() Element of RAT
K116((2 |^ (t + 1)),K118((2 |^ (t + 1)))) is V66() real ext-real set
1 - (s / (2 |^ (t + 1))) is V66() real ext-real Element of REAL
K117((s / (2 |^ (t + 1)))) is V66() real ext-real set
K115(1,K117((s / (2 |^ (t + 1))))) is V66() real ext-real set
1 / (2 |^ (t + 1)) is V66() real ext-real V121() Element of RAT
K116(1,K118((2 |^ (t + 1)))) is V66() real ext-real set
(2 |^ (t + 1)) - s is V66() real ext-real V120() V121() Element of INT
K117(s) is V66() real ext-real V120() set
K115((2 |^ (t + 1)),K117(s)) is V66() real ext-real V120() set
(1 / (2 |^ (t + 1))) * ((2 |^ (t + 1)) - s) is V66() real ext-real V121() Element of RAT
(2 |^ t) / (2 |^ (t + 1)) is V66() real ext-real Element of REAL
K116((2 |^ t),K118((2 |^ (t + 1)))) is V66() real ext-real set
1 * (2 |^ t) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(1 * (2 |^ t)) / (2 * (2 |^ t)) is V66() real ext-real V121() Element of RAT
K118((2 * (2 |^ t))) is V66() real ext-real set
K116((1 * (2 |^ t)),K118((2 * (2 |^ t)))) is V66() real ext-real set
1 / (2 |^ t) is V66() real ext-real Element of REAL
K118((2 |^ t)) is V66() real ext-real set
K116(1,K118((2 |^ t))) is V66() real ext-real set
(1 / 2) * (1 / (2 |^ t)) is V66() real ext-real Element of REAL
1 / (2 * (2 |^ t)) is V66() real ext-real V121() Element of RAT
K116(1,K118((2 * (2 |^ t)))) is V66() real ext-real set
za / (2 |^ (t + 1)) is V66() real ext-real Element of REAL
K116(za,K118((2 |^ (t + 1)))) is V66() real ext-real set
((2 |^ t) + s) / (2 |^ (t + 1)) is V66() real ext-real V121() Element of RAT
K116(((2 |^ t) + s),K118((2 |^ (t + 1)))) is V66() real ext-real set
(((2 |^ t) + s) / (2 |^ (t + 1))) - ((2 |^ (t + 1)) / (2 |^ (t + 1))) is V66() real ext-real V121() Element of RAT
K117(((2 |^ (t + 1)) / (2 |^ (t + 1)))) is V66() real ext-real set
K115((((2 |^ t) + s) / (2 |^ (t + 1))),K117(((2 |^ (t + 1)) / (2 |^ (t + 1))))) is V66() real ext-real set
b is Element of the carrier of E
((s / (2 |^ (t + 1))) - (1 / 2)) * b is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,((s / (2 |^ (t + 1))) - (1 / 2)),b) is set
a is Element of the carrier of E
(1 - (s / (2 |^ (t + 1)))) * a is Element of the carrier of E
K471( the Mult of E,(1 - (s / (2 |^ (t + 1)))),a) is set
(((s / (2 |^ (t + 1))) - (1 / 2)) * b) + ((1 - (s / (2 |^ (t + 1)))) * a) is Element of the carrier of E
((2 |^ (t + 1)) - s) * a is Element of the carrier of E
K471( the Mult of E,((2 |^ (t + 1)) - s),a) is set
(1 / (2 |^ (t + 1))) * (((2 |^ (t + 1)) - s) * a) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),(((2 |^ (t + 1)) - s) * a)) is set
(1 / (2 |^ (t + 1))) * za is V66() real ext-real Element of REAL
((1 / (2 |^ (t + 1))) * za) * b is Element of the carrier of E
K471( the Mult of E,((1 / (2 |^ (t + 1))) * za),b) is set
((1 / (2 |^ (t + 1))) * (((2 |^ (t + 1)) - s) * a)) + (((1 / (2 |^ (t + 1))) * za) * b) is Element of the carrier of E
za * b is Element of the carrier of E
K471( the Mult of E,za,b) is set
(1 / (2 |^ (t + 1))) * (za * b) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),(za * b)) is set
((1 / (2 |^ (t + 1))) * (((2 |^ (t + 1)) - s) * a)) + ((1 / (2 |^ (t + 1))) * (za * b)) is Element of the carrier of E
(((2 |^ (t + 1)) - s) * a) + (za * b) is Element of the carrier of E
(1 / (2 |^ (t + 1))) * ((((2 |^ (t + 1)) - s) * a) + (za * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ (t + 1))),((((2 |^ (t + 1)) - s) * a) + (za * b))) is set
(1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ t)),((((2 |^ (t + 1)) - s) * a) + (za * b))) is set
(1 / 2) * ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b))) is Element of the carrier of E
K471( the Mult of E,(1 / 2),((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b)))) is set
b - a is Element of the carrier of E
- a is Element of the carrier of E
b + (- a) is Element of the carrier of E
(s / (2 |^ (t + 1))) * (b - a) is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),(b - a)) is set
a + ((s / (2 |^ (t + 1))) * (b - a)) is Element of the carrier of E
(s / (2 |^ (t + 1))) * b is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),b) is set
(s / (2 |^ (t + 1))) * a is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ (t + 1))),a) is set
((s / (2 |^ (t + 1))) * b) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
- ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
((s / (2 |^ (t + 1))) * b) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a + (((s / (2 |^ (t + 1))) * b) - ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
(a + ((s / (2 |^ (t + 1))) * b)) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
(a + ((s / (2 |^ (t + 1))) * b)) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
a - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
a + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
(a - ((s / (2 |^ (t + 1))) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
1 * a is Element of the carrier of E
K471( the Mult of E,1,a) is set
(1 * a) - ((s / (2 |^ (t + 1))) * a) is Element of the carrier of E
(1 * a) + (- ((s / (2 |^ (t + 1))) * a)) is Element of the carrier of E
((1 * a) - ((s / (2 |^ (t + 1))) * a)) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
((1 - (s / (2 |^ (t + 1)))) * a) + ((s / (2 |^ (t + 1))) * b) is Element of the carrier of E
((s / (2 |^ (t + 1))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
(((s / (2 |^ (t + 1))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) - (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
- (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
(((s / (2 |^ (t + 1))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + (- (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) is Element of the carrier of E
((((s / (2 |^ (t + 1))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) - (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + ((1 - (s / (2 |^ (t + 1)))) * a) is Element of the carrier of E
((s / (2 |^ (t + 1))) * b) - (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
((s / (2 |^ (t + 1))) * b) + (- (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) is Element of the carrier of E
(((s / (2 |^ (t + 1))) * b) - (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
((((s / (2 |^ (t + 1))) * b) - (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + ((1 - (s / (2 |^ (t + 1)))) * a) is Element of the carrier of E
(s / (2 |^ (t + 1))) - ((s / (2 |^ (t + 1))) - (1 / 2)) is V66() real ext-real Element of REAL
K117(((s / (2 |^ (t + 1))) - (1 / 2))) is V66() real ext-real set
K115((s / (2 |^ (t + 1))),K117(((s / (2 |^ (t + 1))) - (1 / 2)))) is V66() real ext-real set
((s / (2 |^ (t + 1))) - ((s / (2 |^ (t + 1))) - (1 / 2))) * b is Element of the carrier of E
K471( the Mult of E,((s / (2 |^ (t + 1))) - ((s / (2 |^ (t + 1))) - (1 / 2))),b) is set
(((s / (2 |^ (t + 1))) - ((s / (2 |^ (t + 1))) - (1 / 2))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b) is Element of the carrier of E
((((s / (2 |^ (t + 1))) - ((s / (2 |^ (t + 1))) - (1 / 2))) * b) + (((s / (2 |^ (t + 1))) - (1 / 2)) * b)) + ((1 - (s / (2 |^ (t + 1)))) * a) is Element of the carrier of E
(1 / 2) * b is Element of the carrier of E
K471( the Mult of E,(1 / 2),b) is set
((1 / 2) * b) + ((((s / (2 |^ (t + 1))) - (1 / 2)) * b) + ((1 - (s / (2 |^ (t + 1)))) * a)) is Element of the carrier of E
b + ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b))) is Element of the carrier of E
(1 / 2) * (b + ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b)))) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(b + ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b))))) is set
f . (a + ((s / (2 |^ (t + 1))) * (b - a))) is Element of the carrier of F
f . b is Element of the carrier of F
f . ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b))) is Element of the carrier of F
(f . b) + (f . ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b)))) is Element of the carrier of F
(1 / 2) * ((f . b) + (f . ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b))))) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 / 2),((f . b) + (f . ((1 / (2 |^ t)) * ((((2 |^ (t + 1)) - s) * a) + (za * b)))))) is set
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
t is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
a is Element of the carrier of E
b is Element of the carrier of E
f . a is Element of the carrier of F
f . b is Element of the carrier of F
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s / (2 |^ 0) is V66() real ext-real Element of REAL
K118((2 |^ 0)) is V66() real ext-real set
K116(s,K118((2 |^ 0))) is V66() real ext-real set
1 - (s / (2 |^ 0)) is V66() real ext-real Element of REAL
K117((s / (2 |^ 0))) is V66() real ext-real set
K115(1,K117((s / (2 |^ 0)))) is V66() real ext-real set
(1 - (s / (2 |^ 0))) * a is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - (s / (2 |^ 0))),a) is set
(s / (2 |^ 0)) * b is Element of the carrier of E
K471( the Mult of E,(s / (2 |^ 0)),b) is set
((1 - (s / (2 |^ 0))) * a) + ((s / (2 |^ 0)) * b) is Element of the carrier of E
f . (((1 - (s / (2 |^ 0))) * a) + ((s / (2 |^ 0)) * b)) is Element of the carrier of F
(1 - (s / (2 |^ 0))) * (f . a) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - (s / (2 |^ 0))),(f . a)) is set
(s / (2 |^ 0)) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s / (2 |^ 0)),(f . b)) is set
((1 - (s / (2 |^ 0))) * (f . a)) + ((s / (2 |^ 0)) * (f . b)) is Element of the carrier of F
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
1 - s is V66() real ext-real V120() V121() Element of INT
K117(s) is V66() real ext-real V120() set
K115(1,K117(s)) is V66() real ext-real V120() set
(1 - s) * a is Element of the carrier of E
K471( the Mult of E,(1 - s),a) is set
s * b is Element of the carrier of E
K471( the Mult of E,s,b) is set
((1 - s) * a) + (s * b) is Element of the carrier of E
f . (((1 - s) * a) + (s * b)) is Element of the carrier of F
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
(0. E) + (s * b) is Element of the carrier of E
f . ((0. E) + (s * b)) is Element of the carrier of F
f . (s * b) is Element of the carrier of F
s * (f . b) is Element of the carrier of F
K471( the Mult of F,s,(f . b)) is set
0. F is V44(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(0. F) + (s * (f . b)) is Element of the carrier of F
(1 - s) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - s),(f . a)) is set
((1 - s) * (f . a)) + (s * (f . b)) is Element of the carrier of F
1 - s is V66() real ext-real V120() V121() Element of INT
K117(s) is V66() real ext-real V120() set
K115(1,K117(s)) is V66() real ext-real V120() set
(1 - s) * a is Element of the carrier of E
K471( the Mult of E,(1 - s),a) is set
s * b is Element of the carrier of E
K471( the Mult of E,s,b) is set
((1 - s) * a) + (s * b) is Element of the carrier of E
f . (((1 - s) * a) + (s * b)) is Element of the carrier of F
1 * a is Element of the carrier of E
K471( the Mult of E,1,a) is set
0. E is V44(E) Element of the carrier of E
the ZeroF of E is Element of the carrier of E
(1 * a) + (0. E) is Element of the carrier of E
f . ((1 * a) + (0. E)) is Element of the carrier of F
f . (1 * a) is Element of the carrier of F
(1 - s) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - s),(f . a)) is set
0. F is V44(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
((1 - s) * (f . a)) + (0. F) is Element of the carrier of F
s * (f . b) is Element of the carrier of F
K471( the Mult of F,s,(f . b)) is set
((1 - s) * (f . a)) + (s * (f . b)) is Element of the carrier of F
s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
2 |^ s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
s + 1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 |^ (s + 1) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
2 |^ (s + 1) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
s1ta is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s1ta / (2 |^ (s + 1)) is V66() real ext-real Element of REAL
K118((2 |^ (s + 1))) is V66() real ext-real set
K116(s1ta,K118((2 |^ (s + 1)))) is V66() real ext-real set
1 - (s1ta / (2 |^ (s + 1))) is V66() real ext-real Element of REAL
K117((s1ta / (2 |^ (s + 1)))) is V66() real ext-real set
K115(1,K117((s1ta / (2 |^ (s + 1))))) is V66() real ext-real set
(1 - (s1ta / (2 |^ (s + 1)))) * a is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - (s1ta / (2 |^ (s + 1)))),a) is set
(s1ta / (2 |^ (s + 1))) * b is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ (s + 1))),b) is set
((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b) is Element of the carrier of E
f . (((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b)) is Element of the carrier of F
(1 - (s1ta / (2 |^ (s + 1)))) * (f . a) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - (s1ta / (2 |^ (s + 1)))),(f . a)) is set
(s1ta / (2 |^ (s + 1))) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s1ta / (2 |^ (s + 1))),(f . b)) is set
((1 - (s1ta / (2 |^ (s + 1)))) * (f . a)) + ((s1ta / (2 |^ (s + 1))) * (f . b)) is Element of the carrier of F
(2 |^ s) * 2 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
s1ta / (2 |^ s) is V66() real ext-real Element of REAL
K118((2 |^ s)) is V66() real ext-real set
K116(s1ta,K118((2 |^ s))) is V66() real ext-real set
(1 / 2) * (s1ta / (2 |^ s)) is V66() real ext-real Element of REAL
1 * s1ta is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
2 * (2 |^ s) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(1 * s1ta) / (2 * (2 |^ s)) is V66() real ext-real V121() Element of RAT
K118((2 * (2 |^ s))) is V66() real ext-real set
K116((1 * s1ta),K118((2 * (2 |^ s)))) is V66() real ext-real set
s1ta / (2 |^ (s + 1)) is V66() real ext-real Element of REAL
K118((2 |^ (s + 1))) is V66() real ext-real set
K116(s1ta,K118((2 |^ (s + 1)))) is V66() real ext-real set
(2 |^ s) - s1ta is V66() real ext-real V120() V121() Element of INT
K117(s1ta) is V66() real ext-real V120() set
K115((2 |^ s),K117(s1ta)) is V66() real ext-real V120() set
b - a is Element of the carrier of E
- a is Element of the carrier of E
b + (- a) is Element of the carrier of E
(s1ta / (2 |^ (s + 1))) * (b - a) is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ (s + 1))),(b - a)) is set
a + ((s1ta / (2 |^ (s + 1))) * (b - a)) is Element of the carrier of E
f . (a + ((s1ta / (2 |^ (s + 1))) * (b - a))) is Element of the carrier of F
s1ta * b is Element of the carrier of E
K471( the Mult of E,s1ta,b) is set
1 / (2 |^ s) is V66() real ext-real Element of REAL
K116(1,K118((2 |^ s))) is V66() real ext-real set
s1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s1 * a is Element of the carrier of E
K471( the Mult of E,s1,a) is set
(s1 * a) + (s1ta * b) is Element of the carrier of E
(1 / (2 |^ s)) * ((s1 * a) + (s1ta * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),((s1 * a) + (s1ta * b))) is set
f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b))) is Element of the carrier of F
(f . a) + (f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b)))) is Element of the carrier of F
(1 / 2) * ((f . a) + (f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b))))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((f . a) + (f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b)))))) is set
s1 / (2 |^ s) is V66() real ext-real Element of REAL
K116(s1,K118((2 |^ s))) is V66() real ext-real set
(2 |^ s) / (2 |^ s) is V66() real ext-real Element of REAL
K116((2 |^ s),K118((2 |^ s))) is V66() real ext-real set
((2 |^ s) / (2 |^ s)) - (s1ta / (2 |^ s)) is V66() real ext-real Element of REAL
K117((s1ta / (2 |^ s))) is V66() real ext-real set
K115(((2 |^ s) / (2 |^ s)),K117((s1ta / (2 |^ s)))) is V66() real ext-real set
1 - (s1ta / (2 |^ s)) is V66() real ext-real Element of REAL
K115(1,K117((s1ta / (2 |^ s)))) is V66() real ext-real set
(1 / (2 |^ s)) * (s1 * a) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),(s1 * a)) is set
(1 / (2 |^ s)) * (s1ta * b) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),(s1ta * b)) is set
((1 / (2 |^ s)) * (s1 * a)) + ((1 / (2 |^ s)) * (s1ta * b)) is Element of the carrier of E
(s1ta / (2 |^ s)) * b is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ s)),b) is set
((1 / (2 |^ s)) * (s1 * a)) + ((s1ta / (2 |^ s)) * b) is Element of the carrier of E
(s1 / (2 |^ s)) * a is Element of the carrier of E
K471( the Mult of E,(s1 / (2 |^ s)),a) is set
((s1 / (2 |^ s)) * a) + ((s1ta / (2 |^ s)) * b) is Element of the carrier of E
1 - (s1ta / (2 |^ (s + 1))) is V66() real ext-real Element of REAL
K117((s1ta / (2 |^ (s + 1)))) is V66() real ext-real set
K115(1,K117((s1ta / (2 |^ (s + 1))))) is V66() real ext-real set
(1 - (s1ta / (2 |^ (s + 1)))) * a is Element of the carrier of E
K471( the Mult of E,(1 - (s1ta / (2 |^ (s + 1)))),a) is set
(s1ta / (2 |^ (s + 1))) * b is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ (s + 1))),b) is set
((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b) is Element of the carrier of E
f . (((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b)) is Element of the carrier of F
(1 / 2) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . a)) is set
(1 / 2) * (f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b)))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b))))) is set
((1 / 2) * (f . a)) + ((1 / 2) * (f . ((1 / (2 |^ s)) * ((s1 * a) + (s1ta * b))))) is Element of the carrier of F
(1 - (s1ta / (2 |^ s))) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - (s1ta / (2 |^ s))),(f . a)) is set
(s1ta / (2 |^ s)) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s1ta / (2 |^ s)),(f . b)) is set
((1 - (s1ta / (2 |^ s))) * (f . a)) + ((s1ta / (2 |^ s)) * (f . b)) is Element of the carrier of F
(1 / 2) * (((1 - (s1ta / (2 |^ s))) * (f . a)) + ((s1ta / (2 |^ s)) * (f . b))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(((1 - (s1ta / (2 |^ s))) * (f . a)) + ((s1ta / (2 |^ s)) * (f . b)))) is set
((1 / 2) * (f . a)) + ((1 / 2) * (((1 - (s1ta / (2 |^ s))) * (f . a)) + ((s1ta / (2 |^ s)) * (f . b)))) is Element of the carrier of F
(1 / 2) * ((1 - (s1ta / (2 |^ s))) * (f . a)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((1 - (s1ta / (2 |^ s))) * (f . a))) is set
(1 / 2) * ((s1ta / (2 |^ s)) * (f . b)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((s1ta / (2 |^ s)) * (f . b))) is set
((1 / 2) * ((1 - (s1ta / (2 |^ s))) * (f . a))) + ((1 / 2) * ((s1ta / (2 |^ s)) * (f . b))) is Element of the carrier of F
((1 / 2) * (f . a)) + (((1 / 2) * ((1 - (s1ta / (2 |^ s))) * (f . a))) + ((1 / 2) * ((s1ta / (2 |^ s)) * (f . b)))) is Element of the carrier of F
((1 / 2) * (f . a)) + ((1 / 2) * ((1 - (s1ta / (2 |^ s))) * (f . a))) is Element of the carrier of F
(((1 / 2) * (f . a)) + ((1 / 2) * ((1 - (s1ta / (2 |^ s))) * (f . a)))) + ((1 / 2) * ((s1ta / (2 |^ s)) * (f . b))) is Element of the carrier of F
(1 / 2) * (1 - (s1ta / (2 |^ s))) is V66() real ext-real Element of REAL
((1 / 2) * (1 - (s1ta / (2 |^ s)))) * (f . a) is Element of the carrier of F
K471( the Mult of F,((1 / 2) * (1 - (s1ta / (2 |^ s)))),(f . a)) is set
((1 / 2) * (f . a)) + (((1 / 2) * (1 - (s1ta / (2 |^ s)))) * (f . a)) is Element of the carrier of F
(((1 / 2) * (f . a)) + (((1 / 2) * (1 - (s1ta / (2 |^ s)))) * (f . a))) + ((1 / 2) * ((s1ta / (2 |^ s)) * (f . b))) is Element of the carrier of F
(1 / 2) + ((1 / 2) * (1 - (s1ta / (2 |^ s)))) is V66() real ext-real Element of REAL
((1 / 2) + ((1 / 2) * (1 - (s1ta / (2 |^ s))))) * (f . a) is Element of the carrier of F
K471( the Mult of F,((1 / 2) + ((1 / 2) * (1 - (s1ta / (2 |^ s))))),(f . a)) is set
(((1 / 2) + ((1 / 2) * (1 - (s1ta / (2 |^ s))))) * (f . a)) + ((1 / 2) * ((s1ta / (2 |^ s)) * (f . b))) is Element of the carrier of F
(1 - (s1ta / (2 |^ (s + 1)))) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - (s1ta / (2 |^ (s + 1)))),(f . a)) is set
(s1ta / (2 |^ (s + 1))) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s1ta / (2 |^ (s + 1))),(f . b)) is set
((1 - (s1ta / (2 |^ (s + 1)))) * (f . a)) + ((s1ta / (2 |^ (s + 1))) * (f . b)) is Element of the carrier of F
(2 |^ s) + s1ta is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
((2 |^ s) + s1ta) - (2 |^ (s + 1)) is V66() real ext-real V120() V121() Element of INT
K117((2 |^ (s + 1))) is V66() real ext-real V120() set
K115(((2 |^ s) + s1ta),K117((2 |^ (s + 1)))) is V66() real ext-real V120() set
b - a is Element of the carrier of E
- a is Element of the carrier of E
b + (- a) is Element of the carrier of E
(s1ta / (2 |^ (s + 1))) * (b - a) is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ (s + 1))),(b - a)) is set
a + ((s1ta / (2 |^ (s + 1))) * (b - a)) is Element of the carrier of E
f . (a + ((s1ta / (2 |^ (s + 1))) * (b - a))) is Element of the carrier of F
(2 |^ (s + 1)) - s1ta is V66() real ext-real V120() V121() Element of INT
K117(s1ta) is V66() real ext-real V120() set
K115((2 |^ (s + 1)),K117(s1ta)) is V66() real ext-real V120() set
((2 |^ (s + 1)) - s1ta) * a is Element of the carrier of E
K471( the Mult of E,((2 |^ (s + 1)) - s1ta),a) is set
1 / (2 |^ s) is V66() real ext-real Element of REAL
K116(1,K118((2 |^ s))) is V66() real ext-real set
s1 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
s1 * b is Element of the carrier of E
K471( the Mult of E,s1,b) is set
(((2 |^ (s + 1)) - s1ta) * a) + (s1 * b) is Element of the carrier of E
(1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b)) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b))) is set
f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b))) is Element of the carrier of F
(f . b) + (f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b)))) is Element of the carrier of F
(1 / 2) * ((f . b) + (f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b))))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((f . b) + (f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b)))))) is set
s1ta - (2 |^ s) is V66() real ext-real V120() V121() Element of INT
K117((2 |^ s)) is V66() real ext-real V120() set
K115(s1ta,K117((2 |^ s))) is V66() real ext-real V120() set
(2 * (2 |^ s)) - (2 |^ s) is V66() real ext-real V120() V121() Element of INT
K115((2 * (2 |^ s)),K117((2 |^ s))) is V66() real ext-real V120() set
(2 |^ s) / (2 |^ s) is V66() real ext-real Element of REAL
K116((2 |^ s),K118((2 |^ s))) is V66() real ext-real set
(2 |^ (s + 1)) / (2 |^ s) is V66() real ext-real Element of REAL
K116((2 |^ (s + 1)),K118((2 |^ s))) is V66() real ext-real set
1 * (2 |^ s) is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(2 * (2 |^ s)) / (1 * (2 |^ s)) is V66() real ext-real V121() Element of RAT
K118((1 * (2 |^ s))) is V66() real ext-real set
K116((2 * (2 |^ s)),K118((1 * (2 |^ s)))) is V66() real ext-real set
2 / 1 is V66() real ext-real non negative V121() Element of RAT
K118(1) is non empty V66() real ext-real positive non negative set
K116(2,K118(1)) is V66() real ext-real non negative set
(s1ta - (2 |^ s)) / (2 |^ s) is V66() real ext-real Element of REAL
K116((s1ta - (2 |^ s)),K118((2 |^ s))) is V66() real ext-real set
1 - ((s1ta - (2 |^ s)) / (2 |^ s)) is V66() real ext-real Element of REAL
K117(((s1ta - (2 |^ s)) / (2 |^ s))) is V66() real ext-real set
K115(1,K117(((s1ta - (2 |^ s)) / (2 |^ s)))) is V66() real ext-real set
(1 / 2) * (1 - ((s1ta - (2 |^ s)) / (2 |^ s))) is V66() real ext-real Element of REAL
1 - ((1 / 2) * (s1ta / (2 |^ s))) is V66() real ext-real Element of REAL
K117(((1 / 2) * (s1ta / (2 |^ s)))) is V66() real ext-real set
K115(1,K117(((1 / 2) * (s1ta / (2 |^ s))))) is V66() real ext-real set
1 - ((1 * s1ta) / (2 * (2 |^ s))) is V66() real ext-real V121() Element of RAT
K117(((1 * s1ta) / (2 * (2 |^ s)))) is V66() real ext-real set
K115(1,K117(((1 * s1ta) / (2 * (2 |^ s))))) is V66() real ext-real set
1 - (s1ta / (2 |^ (s + 1))) is V66() real ext-real Element of REAL
K117((s1ta / (2 |^ (s + 1)))) is V66() real ext-real set
K115(1,K117((s1ta / (2 |^ (s + 1))))) is V66() real ext-real set
(1 - (s1ta / (2 |^ (s + 1)))) * a is Element of the carrier of E
K471( the Mult of E,(1 - (s1ta / (2 |^ (s + 1)))),a) is set
(s1ta / (2 |^ (s + 1))) * b is Element of the carrier of E
K471( the Mult of E,(s1ta / (2 |^ (s + 1))),b) is set
((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b) is Element of the carrier of E
f . (((1 - (s1ta / (2 |^ (s + 1)))) * a) + ((s1ta / (2 |^ (s + 1))) * b)) is Element of the carrier of F
(1 / 2) * (f . b) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . b)) is set
(1 / 2) * (f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b)))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b))))) is set
((1 / 2) * (f . b)) + ((1 / 2) * (f . ((1 / (2 |^ s)) * ((((2 |^ (s + 1)) - s1ta) * a) + (s1 * b))))) is Element of the carrier of F
(1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),(((2 |^ (s + 1)) - s1ta) * a)) is set
(1 / (2 |^ s)) * (s1 * b) is Element of the carrier of E
K471( the Mult of E,(1 / (2 |^ s)),(s1 * b)) is set
((1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a)) + ((1 / (2 |^ s)) * (s1 * b)) is Element of the carrier of E
f . (((1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a)) + ((1 / (2 |^ s)) * (s1 * b))) is Element of the carrier of F
(1 / 2) * (f . (((1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a)) + ((1 / (2 |^ s)) * (s1 * b)))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . (((1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a)) + ((1 / (2 |^ s)) * (s1 * b))))) is set
((1 / 2) * (f . b)) + ((1 / 2) * (f . (((1 / (2 |^ s)) * (((2 |^ (s + 1)) - s1ta) * a)) + ((1 / (2 |^ s)) * (s1 * b))))) is Element of the carrier of F
(1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta) is V66() real ext-real Element of REAL
((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a is Element of the carrier of E
K471( the Mult of E,((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)),a) is set
(((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + ((1 / (2 |^ s)) * (s1 * b)) is Element of the carrier of E
f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + ((1 / (2 |^ s)) * (s1 * b))) is Element of the carrier of F
(1 / 2) * (f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + ((1 / (2 |^ s)) * (s1 * b)))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + ((1 / (2 |^ s)) * (s1 * b))))) is set
((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + ((1 / (2 |^ s)) * (s1 * b))))) is Element of the carrier of F
(1 / (2 |^ s)) * s1 is V66() real ext-real Element of REAL
((1 / (2 |^ s)) * s1) * b is Element of the carrier of E
K471( the Mult of E,((1 / (2 |^ s)) * s1),b) is set
(((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + (((1 / (2 |^ s)) * s1) * b) is Element of the carrier of E
f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + (((1 / (2 |^ s)) * s1) * b)) is Element of the carrier of F
(1 / 2) * (f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + (((1 / (2 |^ s)) * s1) * b))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + (((1 / (2 |^ s)) * s1) * b)))) is set
((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ s)) * ((2 |^ (s + 1)) - s1ta)) * a) + (((1 / (2 |^ s)) * s1) * b)))) is Element of the carrier of F
(1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - ((s1ta - (2 |^ s)) / (2 |^ s))),(f . a)) is set
((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b) is Element of the carrier of F
K471( the Mult of F,((s1ta - (2 |^ s)) / (2 |^ s)),(f . b)) is set
((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)) is Element of the carrier of F
(1 / 2) * (((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is set
((1 / 2) * (f . b)) + ((1 / 2) * (((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is Element of the carrier of F
(1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) is set
(1 / 2) * (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),(((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is set
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + ((1 / 2) * (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is Element of the carrier of F
((1 / 2) * (f . b)) + (((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + ((1 / 2) * (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is Element of the carrier of F
((1 / 2) * (f . b)) + ((1 / 2) * (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is Element of the carrier of F
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + (((1 / 2) * (f . b)) + ((1 / 2) * (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is Element of the carrier of F
(f . b) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)) is Element of the carrier of F
(1 / 2) * ((f . b) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((f . b) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is set
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + ((1 / 2) * ((f . b) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is Element of the carrier of F
1 * (f . b) is Element of the carrier of F
K471( the Mult of F,1,(f . b)) is set
(1 * (f . b)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)) is Element of the carrier of F
(1 / 2) * ((1 * (f . b)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b))) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((1 * (f . b)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is set
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + ((1 / 2) * ((1 * (f . b)) + (((s1ta - (2 |^ s)) / (2 |^ s)) * (f . b)))) is Element of the carrier of F
1 + ((s1ta - (2 |^ s)) / (2 |^ s)) is V66() real ext-real Element of REAL
(1 + ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . b) is Element of the carrier of F
K471( the Mult of F,(1 + ((s1ta - (2 |^ s)) / (2 |^ s))),(f . b)) is set
(1 / 2) * ((1 + ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . b)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((1 + ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . b))) is set
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + ((1 / 2) * ((1 + ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . b))) is Element of the carrier of F
(1 / 2) * (1 + ((s1ta - (2 |^ s)) / (2 |^ s))) is V66() real ext-real Element of REAL
((1 / 2) * (1 + ((s1ta - (2 |^ s)) / (2 |^ s)))) * (f . b) is Element of the carrier of F
K471( the Mult of F,((1 / 2) * (1 + ((s1ta - (2 |^ s)) / (2 |^ s)))),(f . b)) is set
((1 / 2) * ((1 - ((s1ta - (2 |^ s)) / (2 |^ s))) * (f . a))) + (((1 / 2) * (1 + ((s1ta - (2 |^ s)) / (2 |^ s)))) * (f . b)) is Element of the carrier of F
(1 - (s1ta / (2 |^ (s + 1)))) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - (s1ta / (2 |^ (s + 1)))),(f . a)) is set
(s1ta / (2 |^ (s + 1))) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s1ta / (2 |^ (s + 1))),(f . b)) is set
((1 - (s1ta / (2 |^ (s + 1)))) * (f . a)) + ((s1ta / (2 |^ (s + 1))) * (f . b)) is Element of the carrier of F
s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() set
2 |^ s is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real V120() Element of REAL
t / (2 |^ s) is V66() real ext-real Element of REAL
K118((2 |^ s)) is V66() real ext-real set
K116(t,K118((2 |^ s))) is V66() real ext-real set
1 - (t / (2 |^ s)) is V66() real ext-real Element of REAL
K117((t / (2 |^ s))) is V66() real ext-real set
K115(1,K117((t / (2 |^ s)))) is V66() real ext-real set
(1 - (t / (2 |^ s))) * a is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - (t / (2 |^ s))),a) is set
(t / (2 |^ s)) * b is Element of the carrier of E
K471( the Mult of E,(t / (2 |^ s)),b) is set
((1 - (t / (2 |^ s))) * a) + ((t / (2 |^ s)) * b) is Element of the carrier of E
f . (((1 - (t / (2 |^ s))) * a) + ((t / (2 |^ s)) * b)) is Element of the carrier of F
(1 - (t / (2 |^ s))) * (f . a) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - (t / (2 |^ s))),(f . a)) is set
(t / (2 |^ s)) * (f . b) is Element of the carrier of F
K471( the Mult of F,(t / (2 |^ s)),(f . b)) is set
((1 - (t / (2 |^ s))) * (f . a)) + ((t / (2 |^ s)) * (f . b)) is Element of the carrier of F
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
a is Element of the carrier of E
b is Element of the carrier of E
a + b is Element of the carrier of E
(1 / 2) * (a + b) is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 / 2),(a + b)) is set
f . ((1 / 2) * (a + b)) is Element of the carrier of F
f . a is Element of the carrier of F
f . b is Element of the carrier of F
(f . a) + (f . b) is Element of the carrier of F
(1 / 2) * ((f . a) + (f . b)) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 / 2),((f . a) + (f . b))) is set
K11( the carrier of E, the carrier of E) is set
K10(K11( the carrier of E, the carrier of E)) is set
{ b1 where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : ( b1 is bijective & b1 is (E,E) & b1 . a = a & b1 . b = b ) } is set
a + b is Element of the carrier of E
(1 / 2) * (a + b) is Element of the carrier of E
K471( the Mult of E,(1 / 2),(a + b)) is set
{ ||.((b1 . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| where b1 is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E)) : b1 in H1(E,a,b) } is set
(f . a) + (f . b) is Element of the carrier of F
(1 / 2) * ((f . a) + (f . b)) is Element of the carrier of F
K471( the Mult of F,(1 / 2),((f . a) + (f . b))) is set
(E,((1 / 2) * (a + b))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective (E,E) Element of K10(K11( the carrier of E, the carrier of E))
(F,((1 / 2) * ((f . a) + (f . b)))) is non empty V4() V7( the carrier of F) V8( the carrier of F) Function-like one-to-one total quasi_total onto bijective (F,F) Element of K10(K11( the carrier of F, the carrier of F))
K11( the carrier of F, the carrier of F) is set
K10(K11( the carrier of F, the carrier of F)) is set
f /" is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
K11( the carrier of F, the carrier of E) is set
K10(K11( the carrier of F, the carrier of E)) is set
(E,((1 / 2) * (a + b))) * (f /") is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b)))) is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
(((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
zb is set
n is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
n . ((1 / 2) * (a + b)) is Element of the carrier of E
(n . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b)) is Element of the carrier of E
- ((1 / 2) * (a + b)) is Element of the carrier of E
(n . ((1 / 2) * (a + b))) + (- ((1 / 2) * (a + b))) is Element of the carrier of E
||.((n . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| is V66() real ext-real non negative Element of REAL
rng f is Element of K10( the carrier of F)
K10( the carrier of F) is set
[#] F is non empty non proper Element of K10( the carrier of F)
f " is V4() Function-like set
2 * ((1 / 2) * (a + b)) is Element of the carrier of E
K471( the Mult of E,2,((1 / 2) * (a + b))) is set
(2 * (1 / 2)) * (a + b) is Element of the carrier of E
K471( the Mult of E,(2 * (1 / 2)),(a + b)) is set
(2 * ((1 / 2) * (a + b))) - a is Element of the carrier of E
- a is Element of the carrier of E
(2 * ((1 / 2) * (a + b))) + (- a) is Element of the carrier of E
(2 * ((1 / 2) * (a + b))) - b is Element of the carrier of E
- b is Element of the carrier of E
(2 * ((1 / 2) * (a + b))) + (- b) is Element of the carrier of E
2 * ((1 / 2) * ((f . a) + (f . b))) is Element of the carrier of F
K471( the Mult of F,2,((1 / 2) * ((f . a) + (f . b)))) is set
(2 * (1 / 2)) * ((f . a) + (f . b)) is Element of the carrier of F
K471( the Mult of F,(2 * (1 / 2)),((f . a) + (f . b))) is set
(2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . a) is Element of the carrier of F
- (f . a) is Element of the carrier of F
(2 * ((1 / 2) * ((f . a) + (f . b)))) + (- (f . a)) is Element of the carrier of F
(2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . b) is Element of the carrier of F
- (f . b) is Element of the carrier of F
(2 * ((1 / 2) * ((f . a) + (f . b)))) + (- (f . b)) is Element of the carrier of F
((((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f) . a is Element of the carrier of E
(((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) . (f . a) is Element of the carrier of E
(F,((1 / 2) * ((f . a) + (f . b)))) . (f . a) is Element of the carrier of F
((E,((1 / 2) * (a + b))) * (f /")) . ((F,((1 / 2) * ((f . a) + (f . b)))) . (f . a)) is Element of the carrier of E
((E,((1 / 2) * (a + b))) * (f /")) . (f . b) is Element of the carrier of E
(f /") . (f . b) is Element of the carrier of E
(E,((1 / 2) * (a + b))) . ((f /") . (f . b)) is Element of the carrier of E
(E,((1 / 2) * (a + b))) . b is Element of the carrier of E
((((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f) . b is Element of the carrier of E
(((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) . (f . b) is Element of the carrier of E
(F,((1 / 2) * ((f . a) + (f . b)))) . (f . b) is Element of the carrier of F
((E,((1 / 2) * (a + b))) * (f /")) . ((F,((1 / 2) * ((f . a) + (f . b)))) . (f . b)) is Element of the carrier of E
((E,((1 / 2) * (a + b))) * (f /")) . (f . a) is Element of the carrier of E
(f /") . (f . a) is Element of the carrier of E
(E,((1 / 2) * (a + b))) . ((f /") . (f . a)) is Element of the carrier of E
(E,((1 / 2) * (a + b))) . a is Element of the carrier of E
rng (E,((1 / 2) * (a + b))) is Element of K10( the carrier of E)
K10( the carrier of E) is set
[#] E is non empty non proper Element of K10( the carrier of E)
(E,((1 / 2) * (a + b))) /" is non empty V4() V7( the carrier of E) V7( the carrier of E) V8( the carrier of E) V8( the carrier of E) Function-like total quasi_total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b))) is non empty V4() V7( the carrier of E) V7( the carrier of E) V8( the carrier of E) V8( the carrier of E) Function-like total total quasi_total quasi_total (E,E) Element of K10(K11( the carrier of E, the carrier of E))
dom (E,((1 / 2) * (a + b))) is Element of K10( the carrier of E)
id (dom (E,((1 / 2) * (a + b)))) is V4() V7( dom (E,((1 / 2) * (a + b)))) V8( dom (E,((1 / 2) * (a + b)))) Function-like one-to-one total quasi_total onto bijective Element of K10(K11((dom (E,((1 / 2) * (a + b)))),(dom (E,((1 / 2) * (a + b))))))
K11((dom (E,((1 / 2) * (a + b)))),(dom (E,((1 / 2) * (a + b))))) is set
K10(K11((dom (E,((1 / 2) * (a + b)))),(dom (E,((1 / 2) * (a + b)))))) is set
id E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total (E,E) (E,E) (E,E) Element of K10(K11( the carrier of E, the carrier of E))
id the carrier of E is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of E, the carrier of E))
f * (f /") is non empty V4() V7( the carrier of F) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of F))
id F is non empty V4() V7( the carrier of F) V8( the carrier of F) Function-like total quasi_total (F,F) (F,F) (F,F) Element of K10(K11( the carrier of F, the carrier of F))
id the carrier of F is non empty V4() V7( the carrier of F) V8( the carrier of F) Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of F, the carrier of F))
((E,((1 / 2) * (a + b))) /") * ((((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(F,((1 / 2) * ((f . a) + (f . b)))) * f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
((E,((1 / 2) * (a + b))) * (f /")) * ((F,((1 / 2) * ((f . a) + (f . b)))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (a + b))) /") * (((E,((1 / 2) * (a + b))) * (f /")) * ((F,((1 / 2) * ((f . a) + (f . b)))) * f)) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(f /") * ((F,((1 / 2) * ((f . a) + (f . b)))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(E,((1 / 2) * (a + b))) * ((f /") * ((F,((1 / 2) * ((f . a) + (f . b)))) * f)) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((E,((1 / 2) * (a + b))) /") * ((E,((1 / 2) * (a + b))) * ((f /") * ((F,((1 / 2) * ((f . a) + (f . b)))) * f))) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b)))) * ((f /") * ((F,((1 / 2) * ((f . a) + (f . b)))) * f)) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b)))) * (f /") is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
((((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b)))) * (f /")) * ((F,((1 / 2) * ((f . a) + (f . b)))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
((((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b)))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b)))) is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
(((((E,((1 / 2) * (a + b))) /") * (E,((1 / 2) * (a + b)))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
(f /") * (F,((1 / 2) * ((f . a) + (f . b)))) is non empty V4() V7( the carrier of F) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of F, the carrier of E))
((f /") * (F,((1 / 2) * ((f . a) + (f . b))))) * f is non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of E))
f * (((f /") * (F,((1 / 2) * ((f . a) + (f . b))))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
f * ((f /") * ((F,((1 / 2) * ((f . a) + (f . b)))) * f)) is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
(f * (f /")) * ((F,((1 / 2) * ((f . a) + (f . b)))) * f) is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
zb is complex-membered ext-real-membered real-membered set
((((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f) . ((1 / 2) * (a + b)) is Element of the carrier of E
(((E,((1 / 2) * (a + b))) /") * ((((E,((1 / 2) * (a + b))) * (f /")) * (F,((1 / 2) * ((f . a) + (f . b))))) * f)) . ((1 / 2) * (a + b)) is Element of the carrier of E
((E,((1 / 2) * (a + b))) /") . ((1 / 2) * (a + b)) is Element of the carrier of E
(f * (((f /") * (F,((1 / 2) * ((f . a) + (f . b))))) * f)) . ((1 / 2) * (a + b)) is Element of the carrier of F
f . (((E,((1 / 2) * (a + b))) /") . ((1 / 2) * (a + b))) is Element of the carrier of F
f * ((E,((1 / 2) * (a + b))) /") is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
(f * ((E,((1 / 2) * (a + b))) /")) . ((1 / 2) * (a + b)) is Element of the carrier of F
f . ((1 / 2) * (a + b)) is Element of the carrier of F
(F,((1 / 2) * ((f . a) + (f . b)))) . (f . ((1 / 2) * (a + b))) is Element of the carrier of F
((F,((1 / 2) * ((f . a) + (f . b)))) * f) . ((1 / 2) * (a + b)) is Element of the carrier of F
f * (E,((1 / 2) * (a + b))) is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
(f * (E,((1 / 2) * (a + b)))) . ((1 / 2) * (a + b)) is Element of the carrier of F
(E,((1 / 2) * (a + b))) . ((1 / 2) * (a + b)) is Element of the carrier of E
f . ((E,((1 / 2) * (a + b))) . ((1 / 2) * (a + b))) is Element of the carrier of F
E is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of E is non empty set
F is non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like NORMSTR
the carrier of F is non empty set
K11( the carrier of E, the carrier of F) is set
K10(K11( the carrier of E, the carrier of F)) is set
f is non empty V4() V7( the carrier of E) V8( the carrier of F) Function-like total quasi_total Element of K10(K11( the carrier of E, the carrier of F))
a is Element of the carrier of E
f . a is Element of the carrier of F
b is Element of the carrier of E
f . b is Element of the carrier of F
t is V66() real ext-real set
1 - t is V66() real ext-real Element of REAL
K117(t) is V66() real ext-real set
K115(1,K117(t)) is V66() real ext-real set
(1 - t) * a is Element of the carrier of E
the Mult of E is V4() V7(K11(REAL, the carrier of E)) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of E), the carrier of E))
K11(REAL, the carrier of E) is set
K11(K11(REAL, the carrier of E), the carrier of E) is set
K10(K11(K11(REAL, the carrier of E), the carrier of E)) is set
K471( the Mult of E,(1 - t),a) is set
t * b is Element of the carrier of E
K471( the Mult of E,t,b) is set
((1 - t) * a) + (t * b) is Element of the carrier of E
f . (((1 - t) * a) + (t * b)) is Element of the carrier of F
(1 - t) * (f . a) is Element of the carrier of F
the Mult of F is V4() V7(K11(REAL, the carrier of F)) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(K11(REAL, the carrier of F), the carrier of F))
K11(REAL, the carrier of F) is set
K11(K11(REAL, the carrier of F), the carrier of F) is set
K10(K11(K11(REAL, the carrier of F), the carrier of F)) is set
K471( the Mult of F,(1 - t),(f . a)) is set
t * (f . b) is Element of the carrier of F
K471( the Mult of F,t,(f . b)) is set
((1 - t) * (f . a)) + (t * (f . b)) is Element of the carrier of F
s is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
rng s is complex-membered ext-real-membered real-membered Element of K10(REAL)
lim s is V66() real ext-real Element of REAL
dom f is Element of K10( the carrier of E)
K10( the carrier of E) is set
s * b is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
K11(NAT, the carrier of E) is set
K10(K11(NAT, the carrier of E)) is set
- s is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
1 + (- s) is non empty V4() V7( NAT ) V8( REAL ) Function-like total quasi_total V78() V79() V80() Element of K10(K11(NAT,REAL))
(1 + (- s)) * a is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
((1 + (- s)) * a) + (s * b) is non empty V4() V7( NAT ) V8( the carrier of E) Function-like total quasi_total Element of K10(K11(NAT, the carrier of E))
(1 + (- s)) * (f . a) is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
K11(NAT, the carrier of F) is set
K10(K11(NAT, the carrier of F)) is set
s * (f . b) is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
lim ((1 + (- s)) * a) is Element of the carrier of E
lim (1 + (- s)) is V66() real ext-real Element of REAL
(lim (1 + (- s))) * a is Element of the carrier of E
K471( the Mult of E,(lim (1 + (- s))),a) is set
lim (- s) is V66() real ext-real Element of REAL
- (lim s) is V66() real ext-real Element of REAL
lim (s * b) is Element of the carrier of E
(lim s) * b is Element of the carrier of E
K471( the Mult of E,(lim s),b) is set
lim (((1 + (- s)) * a) + (s * b)) is Element of the carrier of E
((1 - t) * a) + (t * b) is Element of the carrier of E
lim ((1 + (- s)) * (f . a)) is Element of the carrier of F
lim (s * (f . b)) is Element of the carrier of F
f /* (((1 + (- s)) * a) + (s * b)) is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
((1 + (- s)) * (f . a)) + (s * (f . b)) is non empty V4() V7( NAT ) V8( the carrier of F) Function-like total quasi_total Element of K10(K11(NAT, the carrier of F))
n is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
(f /* (((1 + (- s)) * a) + (s * b))) . n is set
(((1 + (- s)) * (f . a)) + (s * (f . b))) . n is set
(1 + (- s)) . n is V66() real ext-real Element of REAL
(- s) . n is V66() real ext-real Element of REAL
1 + ((- s) . n) is V66() real ext-real Element of REAL
s . n is V66() real ext-real Element of REAL
- (s . n) is V66() real ext-real Element of REAL
1 + (- (s . n)) is V66() real ext-real Element of REAL
dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)
m is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
dyadic m is complex-membered ext-real-membered real-membered Element of K10(REAL)
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
rng (((1 + (- s)) * a) + (s * b)) is Element of K10( the carrier of E)
(f /* (((1 + (- s)) * a) + (s * b))) . n is Element of the carrier of F
(((1 + (- s)) * a) + (s * b)) . n is Element of the carrier of E
f . ((((1 + (- s)) * a) + (s * b)) . n) is Element of the carrier of F
((1 + (- s)) * a) . n is Element of the carrier of E
(s * b) . n is Element of the carrier of E
(((1 + (- s)) * a) . n) + ((s * b) . n) is Element of the carrier of E
f . ((((1 + (- s)) * a) . n) + ((s * b) . n)) is Element of the carrier of F
1 - (s . n) is V66() real ext-real Element of REAL
K117((s . n)) is V66() real ext-real set
K115(1,K117((s . n))) is V66() real ext-real set
(1 - (s . n)) * a is Element of the carrier of E
K471( the Mult of E,(1 - (s . n)),a) is set
((1 - (s . n)) * a) + ((s * b) . n) is Element of the carrier of E
f . (((1 - (s . n)) * a) + ((s * b) . n)) is Element of the carrier of F
(s . n) * b is Element of the carrier of E
K471( the Mult of E,(s . n),b) is set
((1 - (s . n)) * a) + ((s . n) * b) is Element of the carrier of E
f . (((1 - (s . n)) * a) + ((s . n) * b)) is Element of the carrier of F
(1 - (s . n)) * (f . a) is Element of the carrier of F
K471( the Mult of F,(1 - (s . n)),(f . a)) is set
(s . n) * (f . b) is Element of the carrier of F
K471( the Mult of F,(s . n),(f . b)) is set
((1 - (s . n)) * (f . a)) + ((s . n) * (f . b)) is Element of the carrier of F
((1 + (- s)) . n) * (f . a) is Element of the carrier of F
K471( the Mult of F,((1 + (- s)) . n),(f . a)) is set
(s * (f . b)) . n is Element of the carrier of F
(((1 + (- s)) . n) * (f . a)) + ((s * (f . b)) . n) is Element of the carrier of F
((1 + (- s)) * (f . a)) . n is Element of the carrier of F
(((1 + (- s)) * (f . a)) . n) + ((s * (f . b)) . n) is Element of the carrier of F
(((1 + (- s)) * (f . a)) + (s * (f . b))) . n is Element of the carrier of F
c17 is epsilon-transitive epsilon-connected ordinal natural V66() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below V120() V121() Element of NAT
c17 / (2 |^ m) is V66() real ext-real V121() Element of RAT
K118((2 |^ m)) is V66() real ext-real set
K116(c17,K118((2 |^ m))) is V66() real ext-real set
rng (((1 + (- s)) * a) + (s * b)) is Element of K10( the carrier of E)
f . (((1 - t) * a) + (t * b)) is Element of the carrier of F
f /. (((1 - t) * a) + (t * b)) is Element of the carrier of F
lim (f /* (((1 + (- s)) * a) + (s * b))) is Element of the carrier of F
((1 - t) * (f . a)) + (t * (f . b)) is Element of the carrier of F