:: PDIFF_1 semantic presentation

REAL is non empty V33() V165() V166() V167() V171() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V165() V166() V167() V168() V169() V170() V171() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V33() V165() V171() set

omega is non empty epsilon-transitive epsilon-connected ordinal V165() V166() V167() V168() V169() V170() V171() set

K6(omega) is set

K6(NAT) is set

K7(NAT,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(NAT,REAL)) is set

K190() is non empty set

K7(K190(),K190()) is set

K7(K7(K190(),K190()),K190()) is set

K6(K7(K7(K190(),K190()),K190())) is set

K7(REAL,K190()) is set

K7(K7(REAL,K190()),K190()) is set

K6(K7(K7(REAL,K190()),K190())) is set

K196() is RLSStruct

the carrier of K196() is set

K6( the carrier of K196()) is set

K200() is Element of K6( the carrier of K196())

K7(K200(),K200()) is set

K7(K7(K200(),K200()),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(K200(),K200()),REAL)) is set

K203() is Element of K6( the carrier of K196())

K7(K203(),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K203(),REAL)) is set

K7(REAL,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(REAL,REAL)) is set

RAT is non empty V33() V165() V166() V167() V168() V171() set

INT is non empty V33() V165() V166() V167() V168() V169() V171() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

K7(1,1) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K6(K7(1,1)) is set

K7(K7(1,1),1) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(1,1),REAL)) is set

K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

K7(2,2) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K7(K7(2,2),REAL) is complex-valued ext-real-valued real-valued set

K6(K7(K7(2,2),REAL)) is set

K456(2) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V207() L20()

the carrier of K456(2) is non empty set

ExtREAL is non empty V166() set

K7(COMPLEX,COMPLEX) is complex-valued set

K6(K7(COMPLEX,COMPLEX)) is set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set

K7(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K6(K7(K7(RAT,RAT),RAT)) is set

K7(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K6(K7(K7(INT,INT),INT)) is set

K7(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K6(K7(K7(NAT,NAT),NAT)) is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V165() V166() V167() V168() V169() V170() V171() set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V139() V164() V165() V166() V167() V168() V169() V170() V171() Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

Seg 1 is V165() V166() V167() V168() V169() V170() Element of K6(NAT)

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL I),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL I),REAL)) is set

W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

n is non empty Relation-like REAL I -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL I),REAL))

i is non empty Relation-like REAL I -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL I),REAL))

r is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

n . r is V11() real ext-real Element of REAL

r . W is V11() real ext-real Element of REAL

i . r is V11() real ext-real Element of REAL

(1,1) is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

REAL 1 is non empty FinSequence-membered FinSequenceSet of REAL

1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL 1),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL 1),REAL)) is set

(1,1) " is Relation-like Function-like set

dom (1,1) is Element of K6((REAL 1))

K6((REAL 1)) is set

rng (1,1) is V165() V166() V167() Element of K6(REAL)

n is set

i is set

(1,1) . n is V11() real ext-real Element of REAL

(1,1) . i is V11() real ext-real Element of REAL

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

<*y*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

<*y*> . 1 is V11() real ext-real Element of REAL

r is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

(1,1) . r is V11() real ext-real Element of REAL

g is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

g . 1 is V11() real ext-real Element of REAL

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

<*Pd*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

<*n*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(1,1) . <*n*> is V11() real ext-real Element of REAL

<*n*> . 1 is V11() real ext-real Element of REAL

((1,1) ") . n is set

n is set

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

<*i*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

r is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

(1,1) . r is V11() real ext-real Element of REAL

r . 1 is V11() real ext-real Element of REAL

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

<*n*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(1,1) . <*n*> is V11() real ext-real Element of REAL

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

((1,1) ") . i is set

<*i*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Seg n is V165() V166() V167() V168() V169() V170() Element of K6(NAT)

(I,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL n),REAL))

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL n),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL n),REAL)) is set

r is set

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

n |-> g is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

y is Relation-like NAT -defined REAL -valued Function-like V40(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n

(I,n) . y is V11() real ext-real Element of REAL

y . I is V11() real ext-real Element of REAL

rng (I,n) is V165() V166() V167() Element of K6(REAL)

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Seg n is V165() V166() V167() V168() V169() V170() Element of K6(NAT)

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

(I,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL n),REAL))

K7((REAL n),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL n),REAL)) is set

dom (I,n) is Element of K6((REAL n))

K6((REAL n)) is set

rng (I,n) is V165() V166() V167() Element of K6(REAL)

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Seg n is V165() V166() V167() V168() V169() V170() Element of K6(NAT)

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

(I,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL n),REAL))

K7((REAL n),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL n),REAL)) is set

dom (I,n) is Element of K6((REAL n))

K6((REAL n)) is set

rng (I,n) is V165() V166() V167() Element of K6(REAL)

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

<*i*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(1,1) . <*i*> is V11() real ext-real Element of REAL

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

((1,1) ") . r is set

<*r*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

K7(REAL,(REAL 1)) is set

K6(K7(REAL,(REAL 1))) is set

dom ((1,1) ") is set

rng ((1,1) ") is set

I is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

I is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

I (#) ((1,1) ") is Relation-like Function-like set

(1,1) (#) (I (#) ((1,1) ")) is Relation-like Function-like set

K7((REAL 1),(REAL 1)) is set

K6(K7((REAL 1),(REAL 1))) is set

n is Relation-like REAL -defined REAL 1 -valued Function-like Element of K6(K7(REAL,(REAL 1)))

n * I is Relation-like REAL -defined REAL 1 -valued Function-like Element of K6(K7(REAL,(REAL 1)))

(n * I) * (1,1) is Relation-like REAL 1 -defined REAL 1 -valued Function-like Element of K6(K7((REAL 1),(REAL 1)))

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL I),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL I),REAL)) is set

n is Relation-like REAL I -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL I),REAL))

n (#) ((1,1) ") is Relation-like Function-like set

K7((REAL I),(REAL 1)) is set

K6(K7((REAL I),(REAL 1))) is set

i is Relation-like REAL -defined REAL 1 -valued Function-like Element of K6(K7(REAL,(REAL 1)))

i * n is Relation-like REAL I -defined REAL 1 -valued Function-like Element of K6(K7((REAL I),(REAL 1)))

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V161() NORMSTR

the carrier of (REAL-NS n) is non empty set

REAL-NS 1 is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V161() NORMSTR

the carrier of (REAL-NS 1) is non empty V2() set

K7( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) is set

K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

(I,n) is non empty Relation-like REAL n -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL n),REAL))

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL n),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL n),REAL)) is set

i is Element of the carrier of (REAL-NS n)

(I,n) . i is V11() real ext-real Element of REAL

<*((I,n) . i)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len H

i is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))

r is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))

g is Element of the carrier of (REAL-NS n)

i . g is Element of the carrier of (REAL-NS 1)

(I,n) . g is V11() real ext-real Element of REAL

<*((I,n) . g)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

r . g is Element of the carrier of (REAL-NS 1)

n is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

i is Relation-like Function-like set

dom i is set

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

i . r is set

Replace (n,I,r) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

i is Relation-like Function-like set

dom i is set

r is Relation-like Function-like set

dom r is set

g is set

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

i . y is set

Replace (n,I,y) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

i . g is set

r . g is set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

i is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

(n,i) is Relation-like Function-like set

K7(REAL,(REAL I)) is set

K6(K7(REAL,(REAL I))) is set

r is set

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

(n,i) . g is set

Replace (i,n,g) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

len i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Pd is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of I -tuples_on REAL

(n,i) . r is set

dom (n,i) is set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL-NS I is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V161() NORMSTR

the carrier of (REAL-NS I) is non empty set

K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS I)) is set

K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS I))) is set

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

i is Element of the carrier of (REAL-NS I)

n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

g is Element of the carrier of (REAL-NS 1)

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

<*y*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

r is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

(I,n,r) is non empty Relation-like REAL -defined REAL I -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL I)))

K7(REAL,(REAL I)) is set

K6(K7(REAL,(REAL I))) is set

(I,n,r) . y is V40(I) Element of REAL I

r is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS I) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS I)))

g is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS I) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS I)))

y is Element of the carrier of (REAL-NS 1)

r . y is Element of the carrier of (REAL-NS I)

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

<*Pd*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

x is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

(I,n,x) is non empty Relation-like REAL -defined REAL I -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL I)))

K7(REAL,(REAL I)) is set

K6(K7(REAL,(REAL I))) is set

(I,n,x) . Pd is V40(I) Element of REAL I

g . y is Element of the carrier of (REAL-NS I)

<*Pd*> . 1 is V11() real ext-real Element of REAL

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

<*f*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

One is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

(I,n,One) is non empty Relation-like REAL -defined REAL I -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL I)))

(I,n,One) . f is V40(I) Element of REAL I

I is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL I),(REAL n)) is set

K6(K7((REAL I),(REAL n))) is set

I is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL I is non empty FinSequence-membered FinSequenceSet of REAL

I -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

REAL n is non empty FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL

K7((REAL I),(REAL n)) is set

K6(K7((REAL I),(REAL n))) is set

i is Relation-like REAL I -defined REAL n -valued Function-like Element of K6(K7((REAL I),(REAL n)))

r is Relation-like NAT -defined REAL -valued Function-like V40(I) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL I

REAL-NS I is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V161() NORMSTR

the carrier of (REAL-NS I) is non empty V2() set

REAL-NS n is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V161() NORMSTR

the carrier of (REAL-NS n) is non empty V2() set

K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n)) is set

K6(K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n))) is set

g is Relation-like the carrier of (REAL-NS I) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))

y is Element of the carrier of (REAL-NS I)

diff (g,y) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))

R_NormSpace_of_BoundedLinearOperators ((REAL-NS I),(REAL-NS n)) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() RealNormSpace-like V161() NORMSTR

BoundedLinearOperators ((REAL-NS I),(REAL-NS n)) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))))

R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS I),(REAL-NS n)) is non empty functional Element of K6( the carrier of K313( the carrier of (REAL-NS I),(REAL-NS n)))

K313( the carrier of (REAL-NS I),(REAL-NS n)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)) is non empty functional FUNCTION_DOMAIN of the carrier of (REAL-NS I), the carrier of (REAL-NS n)

FuncZero ( the carrier of (REAL-NS I),(REAL-NS n)) is Relation-like the carrier of (REAL-NS I) -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))

0. (REAL-NS n) is V52( REAL-NS n) Element of the carrier of (REAL-NS n)

K228( the carrier of (REAL-NS n), the carrier of (REAL-NS I),(0. (REAL-NS n))) is non empty Relation-like the carrier of (REAL-NS I) -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))

FuncAdd ( the carrier of (REAL-NS I),(REAL-NS n)) is Relation-like K7((Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) -defined Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7((Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))))

K7((Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) is set

K7(K7((Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) is set

K6(K7(K7((Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))))) is set

FuncExtMult ( the carrier of (REAL-NS I),(REAL-NS n)) is Relation-like K7(REAL,(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) -defined Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))))

K7(REAL,(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) is set

K7(K7(REAL,(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))) is set

K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))),(Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))))) is set

RLSStruct(# (Funcs ( the carrier of (REAL-NS I), the carrier of (REAL-NS n))),(FuncZero ( the carrier of (REAL-NS I),(REAL-NS n))),(FuncAdd ( the carrier of (REAL-NS I),(REAL-NS n))),(FuncExtMult ( the carrier of (REAL-NS I),(REAL-NS n))) #) is strict RLSStruct

the carrier of K313( the carrier of (REAL-NS I),(REAL-NS n)) is non empty set

K6( the carrier of K313( the carrier of (REAL-NS I),(REAL-NS n))) is set

K199(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS I),(REAL-NS n))

K197(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is Relation-like K7((LinearOperators ((REAL-NS I),(REAL-NS n))),(LinearOperators ((REAL-NS I),(REAL-NS n)))) -defined LinearOperators ((REAL-NS I),(REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7((LinearOperators ((REAL-NS I),(REAL-NS n))),(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n)))))

K7((LinearOperators ((REAL-NS I),(REAL-NS n))),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K7(K7((LinearOperators ((REAL-NS I),(REAL-NS n))),(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K6(K7(K7((LinearOperators ((REAL-NS I),(REAL-NS n))),(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n))))) is set

K198(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS I),(REAL-NS n)))) -defined LinearOperators ((REAL-NS I),(REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n)))))

K7(REAL,(LinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K7(K7(REAL,(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K6(K7(K7(REAL,(LinearOperators ((REAL-NS I),(REAL-NS n)))),(LinearOperators ((REAL-NS I),(REAL-NS n))))) is set

RLSStruct(# (LinearOperators ((REAL-NS I),(REAL-NS n))),K199(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))),K197(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))),K198(K313( the carrier of (REAL-NS I),(REAL-NS n)),(LinearOperators ((REAL-NS I),(REAL-NS n)))) #) is V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))) is non empty set

K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K199((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is Element of BoundedLinearOperators ((REAL-NS I),(REAL-NS n))

K197((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is Relation-like K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS I),(REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))))

K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K7(K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K6(K7(K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n))))) is set

K198((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS I),(REAL-NS n)) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))))

K7(REAL,(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K7(K7(REAL,(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))) is set

K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n))))) is set

BoundedLinearOperatorsNorm ((REAL-NS I),(REAL-NS n)) is non empty Relation-like BoundedLinearOperators ((REAL-NS I),(REAL-NS n)) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),REAL))

K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),REAL)) is set

NORMSTR(# (BoundedLinearOperators ((REAL-NS I),(REAL-NS n))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),K198((R_VectorSpace_of_LinearOperators ((REAL-NS I),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))),(BoundedLinearOperatorsNorm ((REAL-NS I),(REAL-NS n))) #) is strict NORMSTR

the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS I),(REAL-NS n))) is non empty set

f is Relation-like the carrier of (REAL-NS I) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))

One is Element of the carrier of (REAL-NS I)

Pd is non empty Relation-like REAL I -defined REAL n -valued Function-like total quasi_total Element of K6(K7((REAL I),(REAL n)))

diff (f,One) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))

x is Relation-like the carrier of (REAL-NS I) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS I), the carrier of (REAL-NS n)))

I is Element of the carrier of (REAL-NS I)

x is non empty Relation-like REAL I -defined REAL n -valued Function-like total quasi_total Element of K6(K7((REAL I),(REAL n)))

diff (x,I) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS I),(REAL-NS n)))

I is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

n is Element of the carrier of (REAL-NS 1)

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

I . i is V40(1) Element of REAL 1

r is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

<*i*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

sqr r is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of 1 -tuples_on REAL

Sum (sqr r) is V11() real ext-real Element of REAL

sqrt (Sum (sqr r)) is V11() real ext-real Element of REAL

i ^2 is V11() real ext-real Element of REAL

<*(i ^2)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum <*(i ^2)*> is V11() real ext-real Element of REAL

sqrt (Sum <*(i ^2)*>) is V11() real ext-real Element of REAL

sqrt (i ^2) is V11() real ext-real Element of REAL

||.n.|| is V11() real ext-real Element of REAL

|.r.| is V11() real ext-real non negative Element of REAL

sqr r is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum (sqr r) is V11() real ext-real Element of REAL

sqrt (Sum (sqr r)) is V11() real ext-real Element of REAL

abs i is V11() real ext-real Element of REAL

n is Element of the carrier of (REAL-NS 1)

i is Element of the carrier of (REAL-NS 1)

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

I . r is V40(1) Element of REAL 1

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

I . g is V40(1) Element of REAL 1

<*g*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Pd is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

<*r*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

y is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n - i is Element of the carrier of (REAL-NS 1)

<*r*> - <*g*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

r - g is V11() real ext-real Element of REAL

<*(r - g)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

I . (r - g) is V40(1) Element of REAL 1

n is Element of the carrier of (REAL-NS 1)

i is Element of the carrier of (REAL-NS 1)

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

I . r is V40(1) Element of REAL 1

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

I . g is V40(1) Element of REAL 1

<*g*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Pd is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

<*r*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

y is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n + i is Element of the carrier of (REAL-NS 1)

<*r*> + <*g*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

r + g is V11() real ext-real Element of REAL

<*(r + g)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

I . (r + g) is V40(1) Element of REAL 1

n is Element of the carrier of (REAL-NS 1)

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

I . i is V40(1) Element of REAL 1

g is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

<*i*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

r * n is Element of the carrier of (REAL-NS 1)

r * g is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

r * i is V11() real ext-real Element of REAL

<*(r * i)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

I . (r * i) is V40(1) Element of REAL 1

n is Element of the carrier of (REAL-NS 1)

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

I . i is V40(1) Element of REAL 1

(- 1) * n is Element of the carrier of (REAL-NS 1)

(- 1) * i is V11() real ext-real Element of REAL

I . ((- 1) * i) is V40(1) Element of REAL 1

- n is Element of the carrier of (REAL-NS 1)

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

I . (- i) is V40(1) Element of REAL 1

n is Element of the carrier of (REAL-NS 1)

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

I . i is V40(1) Element of REAL 1

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

r * n is Element of the carrier of (REAL-NS 1)

r * i is V11() real ext-real Element of REAL

I . (r * i) is V40(1) Element of REAL 1

g is Element of the carrier of (REAL-NS 1)

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

I . y is V40(1) Element of REAL 1

- g is Element of the carrier of (REAL-NS 1)

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

I . (- y) is V40(1) Element of REAL 1

Pd is Element of the carrier of (REAL-NS 1)

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

I . f is V40(1) Element of REAL 1

x is Element of the carrier of (REAL-NS 1)

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

I . One is V40(1) Element of REAL 1

Pd - x is Element of the carrier of (REAL-NS 1)

f - One is V11() real ext-real Element of REAL

I . (f - One) is V40(1) Element of REAL 1

n is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

n is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

i is Element of the carrier of (REAL-NS 1)

n . i is V11() real ext-real Element of REAL

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

I is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

g is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . g is V11() real ext-real Element of REAL

I . (n . g) is V40(1) Element of REAL 1

I . r is V40(1) Element of REAL 1

||.i.|| is V11() real ext-real Element of REAL

abs r is V11() real ext-real Element of REAL

i is Element of the carrier of (REAL-NS 1)

r is Element of the carrier of (REAL-NS 1)

n . i is V11() real ext-real Element of REAL

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

n . r is V11() real ext-real Element of REAL

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

x is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . x is V11() real ext-real Element of REAL

I . (n . x) is V40(1) Element of REAL 1

I . y is V40(1) Element of REAL 1

Pd is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . Pd is V11() real ext-real Element of REAL

I . (n . Pd) is V40(1) Element of REAL 1

I . g is V40(1) Element of REAL 1

i + r is Element of the carrier of (REAL-NS 1)

n . (i + r) is V11() real ext-real Element of REAL

g + y is V11() real ext-real Element of REAL

I . (g + y) is V40(1) Element of REAL 1

n . (I . (g + y)) is V11() real ext-real Element of REAL

i is Element of the carrier of (REAL-NS 1)

n . i is V11() real ext-real Element of REAL

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

y is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . y is V11() real ext-real Element of REAL

I . (n . y) is V40(1) Element of REAL 1

I . r is V40(1) Element of REAL 1

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

g * i is Element of the carrier of (REAL-NS 1)

n . (g * i) is V11() real ext-real Element of REAL

g * r is V11() real ext-real Element of REAL

I . (g * r) is V40(1) Element of REAL 1

n . (I . (g * r)) is V11() real ext-real Element of REAL

i is Element of the carrier of (REAL-NS 1)

n . i is V11() real ext-real Element of REAL

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

I . r is V40(1) Element of REAL 1

g is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . g is V11() real ext-real Element of REAL

I . (n . g) is V40(1) Element of REAL 1

- i is Element of the carrier of (REAL-NS 1)

n . (- i) is V11() real ext-real Element of REAL

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

I . (- r) is V40(1) Element of REAL 1

n . (I . (- r)) is V11() real ext-real Element of REAL

i is Element of the carrier of (REAL-NS 1)

n . i is V11() real ext-real Element of REAL

r is Element of the carrier of (REAL-NS 1)

n . r is V11() real ext-real Element of REAL

i - r is Element of the carrier of (REAL-NS 1)

n . (i - r) is V11() real ext-real Element of REAL

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

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

g - y is V11() real ext-real Element of REAL

x is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . x is V11() real ext-real Element of REAL

I . (n . x) is V40(1) Element of REAL 1

I . y is V40(1) Element of REAL 1

Pd is Relation-like NAT -defined REAL -valued Function-like V40(1) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 1

n . Pd is V11() real ext-real Element of REAL

I . (n . Pd) is V40(1) Element of REAL 1

I . g is V40(1) Element of REAL 1

I . (g - y) is V40(1) Element of REAL 1

n . (I . (g - y)) is V11() real ext-real Element of REAL

K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is set

K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set

n is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

i is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

r is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like RestFunc-like Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

i * r is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of (REAL-NS 1),REAL))

K7( the carrier of (REAL-NS 1),REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of (REAL-NS 1),REAL)) is set

(i * r) * n is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

g is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

i * g is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

(i * g) * n is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom y is V165() V166() V167() Element of K6(REAL)

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

0. (REAL-NS 1) is V52( REAL-NS 1) Element of the carrier of (REAL-NS 1)

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

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

abs f is V11() real ext-real Element of REAL

(abs f) " is V11() real ext-real Element of REAL

y . f is V11() real ext-real Element of REAL

abs (y . f) is V11() real ext-real Element of REAL

((abs f) ") * (abs (y . f)) is V11() real ext-real Element of REAL

n . f is V40(1) Element of REAL 1

x is ext-real Element of ExtREAL

|.x.| is ext-real Element of ExtREAL

One is Element of the carrier of (REAL-NS 1)

||.One.|| is V11() real ext-real Element of REAL

n * i is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

id (dom (1,1)) is Relation-like dom (1,1) -defined dom (1,1) -valued Function-like one-to-one total quasi_total Element of K6(K7((dom (1,1)),(dom (1,1))))

K7((dom (1,1)),(dom (1,1))) is set

K6(K7((dom (1,1)),(dom (1,1)))) is set

id (REAL 1) is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like one-to-one total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

dom (i * g) is Element of K6((REAL 1))

dom r is Element of K6( the carrier of (REAL-NS 1))

K6( the carrier of (REAL-NS 1)) is set

r /. One is Element of the carrier of (REAL-NS 1)

r . One is set

id the carrier of (REAL-NS 1) is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like one-to-one total quasi_total Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

(id the carrier of (REAL-NS 1)) * r is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

((id the carrier of (REAL-NS 1)) * r) . (n . f) is set

(n * i) * r is Relation-like the carrier of (REAL-NS 1) -defined REAL 1 -valued Function-like Element of K6(K7( the carrier of (REAL-NS 1),(REAL 1)))

K7( the carrier of (REAL-NS 1),(REAL 1)) is set

K6(K7( the carrier of (REAL-NS 1),(REAL 1))) is set

((n * i) * r) . (n . f) is set

r . (n . f) is set

(n * i) . (r . (n . f)) is set

dom i is Element of K6((REAL 1))

g . One is set

i . (g . One) is V11() real ext-real Element of REAL

n . (i . (g . One)) is V40(1) Element of REAL 1

(i * g) . (n . f) is V11() real ext-real Element of REAL

n . ((i * g) . (n . f)) is V40(1) Element of REAL 1

n . (y . f) is V40(1) Element of REAL 1

||.(r /. One).|| is V11() real ext-real Element of REAL

||.One.|| " is V11() real ext-real Element of REAL

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

abs f is V11() real ext-real Element of REAL

(abs f) " is V11() real ext-real Element of REAL

y . f is V11() real ext-real Element of REAL

abs (y . f) is V11() real ext-real Element of REAL

((abs f) ") * (abs (y . f)) is V11() real ext-real Element of REAL

Pd is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))

Pd " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

y /* Pd is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(Pd ") (#) (y /* Pd) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

lim ((Pd ") (#) (y /* Pd)) is V11() real ext-real Element of REAL

x is V11() real ext-real set

lim Pd is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V165() V166() V167() V168() V169() V170() V171() Element of REAL

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

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

x is V11() real ext-real set

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Pd . R is V11() real ext-real Element of REAL

rng Pd is V165() V166() V167() Element of K6(REAL)

abs (Pd . R) is V11() real ext-real Element of REAL

(abs (Pd . R)) " is V11() real ext-real Element of REAL

y . (Pd . R) is V11() real ext-real Element of REAL

abs (y . (Pd . R)) is V11() real ext-real Element of REAL

((abs (Pd . R)) ") * (abs (y . (Pd . R))) is V11() real ext-real Element of REAL

(y /* Pd) . R is V11() real ext-real Element of REAL

abs ((y /* Pd) . R) is V11() real ext-real Element of REAL

((abs (Pd . R)) ") * (abs ((y /* Pd) . R)) is V11() real ext-real Element of REAL

abs Pd is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs Pd) . R is V11() real ext-real Element of REAL

((abs Pd) . R) " is V11() real ext-real Element of REAL

(((abs Pd) . R) ") * (abs ((y /* Pd) . R)) is V11() real ext-real Element of REAL

(abs Pd) " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((abs Pd) ") . R is V11() real ext-real Element of REAL

(((abs Pd) ") . R) * (abs ((y /* Pd) . R)) is V11() real ext-real Element of REAL

abs (Pd ") is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs (Pd ")) . R is V11() real ext-real Element of REAL

((abs (Pd ")) . R) * (abs ((y /* Pd) . R)) is V11() real ext-real Element of REAL

(Pd ") . R is V11() real ext-real Element of REAL

abs ((Pd ") . R) is V11() real ext-real Element of REAL

(abs ((Pd ") . R)) * (abs ((y /* Pd) . R)) is V11() real ext-real Element of REAL

((Pd ") . R) * ((y /* Pd) . R) is V11() real ext-real Element of REAL

abs (((Pd ") . R) * ((y /* Pd) . R)) is V11() real ext-real Element of REAL

((Pd ") (#) (y /* Pd)) . R is V11() real ext-real Element of REAL

(((Pd ") (#) (y /* Pd)) . R) - 0 is V11() real ext-real Element of REAL

abs ((((Pd ") (#) (y /* Pd)) . R) - 0) is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

(Pd . R) - 0 is V11() real ext-real Element of REAL

abs ((Pd . R) - 0) is V11() real ext-real Element of REAL

r is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total V158( REAL-NS 1, REAL-NS 1) V159( REAL-NS 1, REAL-NS 1) Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

i * r is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of (REAL-NS 1),REAL))

K7( the carrier of (REAL-NS 1),REAL) is complex-valued ext-real-valued real-valued set

K6(K7( the carrier of (REAL-NS 1),REAL)) is set

(i * r) * n is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

g is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

i * g is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

(i * g) * n is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (i * g) is Element of K6((REAL 1))

y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

y . 1 is V11() real ext-real Element of REAL

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

dom ((i * g) * n) is V165() V166() V167() Element of K6(REAL)

dom g is Element of K6((REAL 1))

n . 1 is V40(1) Element of REAL 1

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

y . f is V11() real ext-real Element of REAL

Pd * f is V11() real ext-real Element of REAL

dom n is V165() V166() V167() Element of K6(REAL)

f * 1 is V11() real ext-real Element of REAL

n . (f * 1) is V40(1) Element of REAL 1

(i * r) . (n . (f * 1)) is V11() real ext-real Element of REAL

x is Element of the carrier of (REAL-NS 1)

f * x is Element of the carrier of (REAL-NS 1)

(i * r) . (f * x) is V11() real ext-real Element of REAL

r . (f * x) is Element of the carrier of (REAL-NS 1)

i . (r . (f * x)) is V11() real ext-real Element of REAL

r . x is Element of the carrier of (REAL-NS 1)

f * (r . x) is Element of the carrier of (REAL-NS 1)

i . (f * (r . x)) is V11() real ext-real Element of REAL

i . (r . x) is V11() real ext-real Element of REAL

f * (i . (r . x)) is V11() real ext-real Element of REAL

(i * g) . (n . 1) is V11() real ext-real Element of REAL

f * ((i * g) . (n . 1)) is V11() real ext-real Element of REAL

n is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

i is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

n * r is Relation-like REAL -defined REAL 1 -valued Function-like Element of K6(K7(REAL,(REAL 1)))

(n * r) * i is Relation-like REAL 1 -defined REAL 1 -valued Function-like Element of K6(K7((REAL 1),(REAL 1)))

g is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

n * g is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 1)))

(n * g) * i is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

0. (REAL-NS 1) is V52( REAL-NS 1) Element of the carrier of (REAL-NS 1)

K7(NAT, the carrier of (REAL-NS 1)) is set

K6(K7(NAT, the carrier of (REAL-NS 1))) is set

y is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

Pd is non empty Relation-like NAT -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total non-zero 0. (REAL-NS 1) -convergent Element of K6(K7(NAT, the carrier of (REAL-NS 1)))

y /* Pd is non empty Relation-like NAT -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS 1)))

||.Pd.|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

||.Pd.|| " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(||.Pd.|| ") (#) (y /* Pd) is non empty Relation-like NAT -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS 1)))

lim ((||.Pd.|| ") (#) (y /* Pd)) is Element of the carrier of (REAL-NS 1)

lim Pd is Element of the carrier of (REAL-NS 1)

x is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

f is V11() real ext-real set

One is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Pd . I is Element of the carrier of (REAL-NS 1)

(Pd . I) - (0. (REAL-NS 1)) is Element of the carrier of (REAL-NS 1)

||.((Pd . I) - (0. (REAL-NS 1))).|| is V11() real ext-real Element of REAL

||.(Pd . I).|| is V11() real ext-real Element of REAL

x . I is V11() real ext-real Element of REAL

i . (Pd . I) is V11() real ext-real Element of REAL

(x . I) - 0 is V11() real ext-real Element of REAL

abs ((x . I) - 0) is V11() real ext-real Element of REAL

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

x . I is V11() real ext-real Element of REAL

(x . I) - 0 is V11() real ext-real Element of REAL

abs ((x . I) - 0) is V11() real ext-real Element of REAL

lim x is V11() real ext-real Element of REAL

f is set

One is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

x . One is V11() real ext-real Element of REAL

abs (x . One) is V11() real ext-real Element of REAL

Pd . One is Element of the carrier of (REAL-NS 1)

||.(Pd . One).|| is V11() real ext-real Element of REAL

i . (Pd . One) is V11() real ext-real Element of REAL

x . f is V11() real ext-real Element of REAL

i * n is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))

rng Pd is Element of K6( the carrier of (REAL-NS 1))

K6( the carrier of (REAL-NS 1)) is set

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

Pd . x is Element of the carrier of (REAL-NS 1)

f is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))

r /* f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(r /* f) . x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

r . (f . x) is V11() real ext-real Element of REAL

i . (Pd . x) is V11() real ext-real Element of REAL

r . (i . (Pd . x)) is V11() real ext-real Element of REAL

g . (i . (Pd . x)) is V11() real ext-real Element of REAL

(i * n) . (g . (i . (Pd . x))) is V11() real ext-real Element of REAL

g * i is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))

(g * i) . (Pd . x) is V11() real ext-real Element of REAL

(i * n) . ((g * i) . (Pd . x)) is V11() real ext-real Element of REAL

n . ((g * i) . (Pd . x)) is V40(1) Element of REAL 1

i . (n . ((g * i) . (Pd . x))) is V11() real ext-real Element of REAL

n * (g * i) is non empty Relation-like REAL 1 -defined REAL 1 -valued Function-like total quasi_total Element of K6(K7((REAL 1),(REAL 1)))

(n * (g * i)) . (Pd . x) is set

i . ((n * (g * i)) . (Pd . x)) is V11() real ext-real Element of REAL

dom Pd is V165() V166() V167() V168() V169() V170() Element of K6(NAT)

y . (Pd . x) is set

One is Relation-like Function-like set

Pd (#) One is Relation-like Function-like set

(Pd (#) One) . x is set

dom y is Element of K6( the carrier of (REAL-NS 1))

(y /* Pd) . x is Element of the carrier of (REAL-NS 1)

i . ((y /* Pd) . x) is V11() real ext-real Element of REAL

||.(Pd . x).|| is V11() real ext-real Element of REAL

||.((||.Pd.|| ") (#) (y /* Pd)).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

||.((||.Pd.|| ") (#) (y /* Pd)).|| . x is V11() real ext-real Element of REAL

((||.Pd.|| ") (#) (y /* Pd)) . x is Element of the carrier of (REAL-NS 1)

||.(((||.Pd.|| ") (#) (y /* Pd)) . x).|| is V11() real ext-real Element of REAL

(||.Pd.|| ") . x is V11() real ext-real Element of REAL

((||.Pd.|| ") . x) * ((y /* Pd) . x) is Element of the carrier of (REAL-NS 1)

||.(((||.Pd.|| ") . x) * ((y /* Pd) . x)).|| is V11() real ext-real Element of REAL

abs ((||.Pd.|| ") . x) is V11() real ext-real Element of REAL

||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

(abs ((||.Pd.|| ") . x)) * ||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

||.Pd.|| . x is V11() real ext-real Element of REAL

(||.Pd.|| . x) " is V11() real ext-real Element of REAL

abs ((||.Pd.|| . x) ") is V11() real ext-real Element of REAL

(abs ((||.Pd.|| . x) ")) * ||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

||.(Pd . x).|| " is V11() real ext-real Element of REAL

abs (||.(Pd . x).|| ") is V11() real ext-real Element of REAL

(abs (||.(Pd . x).|| ")) * ||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

(||.(Pd . x).|| ") * ||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

abs (f . x) is V11() real ext-real Element of REAL

(abs (f . x)) " is V11() real ext-real Element of REAL

((abs (f . x)) ") * ||.((y /* Pd) . x).|| is V11() real ext-real Element of REAL

abs ((r /* f) . x) is V11() real ext-real Element of REAL

((abs (f . x)) ") * (abs ((r /* f) . x)) is V11() real ext-real Element of REAL

abs (r /* f) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs (r /* f)) . x is V11() real ext-real Element of REAL

((abs (f . x)) ") * ((abs (r /* f)) . x) is V11() real ext-real Element of REAL

abs f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs f) . x is V11() real ext-real Element of REAL

((abs f) . x) " is V11() real ext-real Element of REAL

(((abs f) . x) ") * ((abs (r /* f)) . x) is V11() real ext-real Element of REAL

(abs f) " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((abs f) ") . x is V11() real ext-real Element of REAL

(((abs f) ") . x) * ((abs (r /* f)) . x) is V11() real ext-real Element of REAL

((abs f) ") (#) (abs (r /* f)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(((abs f) ") (#) (abs (r /* f))) . x is V11() real ext-real Element of REAL

f " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

abs (f ") is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs (f ")) (#) (abs (r /* f)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((abs (f ")) (#) (abs (r /* f))) . x is V11() real ext-real Element of REAL

(f ") (#) (r /* f) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

abs ((f ") (#) (r /* f)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(abs ((f ") (#) (r /* f))) . x is V11() real ext-real Element of REAL

lim ((f ") (#) (r /* f)) is V11() real ext-real Element of REAL

lim (abs ((f ") (#) (r /* f))) is V11() real ext-real Element of REAL

abs (lim ((f ") (#) (r /* f))) is V11() real ext-real Element of REAL

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

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

I is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V139() V164() V165() V166() V167() V168() V169() V170() Element of NAT

||.((||.Pd.|| ") (#) (y /* Pd)).|| . x is V11() real ext-real Element of REAL

(||.((||.Pd.|| ") (#) (y /* Pd)).|| . x) - 0 is V11() real ext-real Element of REAL

abs ((||.((||.Pd