:: MAZURULM semantic presentation

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

{ b

{ ||.((b