:: PDIFF_7 semantic presentation

K6(REAL) is set

K7(NAT,()) is set
K6(K7(NAT,())) is set
COMPLEX is non empty non finite complex-membered V205() set

K6(omega) is set
K6(NAT) is 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

K6(K7(K7(K200(),K200()),REAL)) is set
K203() is Element of K6( the carrier of K196())

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

K6(K7(1,1)) is set

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

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

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

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

the carrier of () is non empty set

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

the carrier of () is non empty V2() set

BoundedLinearOperators ((),()) is non empty Element of K6( the carrier of ())

LinearOperators ((),()) is non empty functional Element of K6( the carrier of K318( the carrier of (),()))

Funcs ( the carrier of (), the carrier of ()) is non empty functional FUNCTION_DOMAIN of the carrier of (), the carrier of ()
FuncZero ( the carrier of (),()) is Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total Element of Funcs ( the carrier of (), the carrier of ())
0. () is V52( REAL-NS 1) Element of the carrier of ()
K214( the carrier of (), the carrier of (),(0. ())) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total Element of K6(K7( the carrier of (), the carrier of ()))
K7( the carrier of (), the carrier of ()) is set
K6(K7( the carrier of (), the carrier of ())) is set
FuncAdd ( the carrier of (),()) is Relation-like K7((Funcs ( the carrier of (), the carrier of ())),(Funcs ( the carrier of (), the carrier of ()))) -defined Funcs ( the carrier of (), the carrier of ()) -valued Function-like total quasi_total Element of K6(K7(K7((Funcs ( the carrier of (), the carrier of ())),(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ()))))
K7((Funcs ( the carrier of (), the carrier of ())),(Funcs ( the carrier of (), the carrier of ()))) is set
K7(K7((Funcs ( the carrier of (), the carrier of ())),(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ()))) is set
K6(K7(K7((Funcs ( the carrier of (), the carrier of ())),(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ())))) is set
FuncExtMult ( the carrier of (),()) is Relation-like K7(REAL,(Funcs ( the carrier of (), the carrier of ()))) -defined Funcs ( the carrier of (), the carrier of ()) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ()))))
K7(REAL,(Funcs ( the carrier of (), the carrier of ()))) is set
K7(K7(REAL,(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ()))) is set
K6(K7(K7(REAL,(Funcs ( the carrier of (), the carrier of ()))),(Funcs ( the carrier of (), the carrier of ())))) is set
RLSStruct(# (Funcs ( the carrier of (), the carrier of ())),(FuncZero ( the carrier of (),())),(FuncAdd ( the carrier of (),())),(FuncExtMult ( the carrier of (),())) #) is strict RLSStruct
the carrier of K318( the carrier of (),()) is non empty set
K6( the carrier of K318( the carrier of (),())) is set
K199(K318( the carrier of (),()),(LinearOperators ((),()))) is Relation-like Function-like Element of LinearOperators ((),())
K197(K318( the carrier of (),()),(LinearOperators ((),()))) is Relation-like K7((LinearOperators ((),())),(LinearOperators ((),()))) -defined LinearOperators ((),()) -valued Function-like total quasi_total Element of K6(K7(K7((LinearOperators ((),())),(LinearOperators ((),()))),(LinearOperators ((),()))))
K7((LinearOperators ((),())),(LinearOperators ((),()))) is set
K7(K7((LinearOperators ((),())),(LinearOperators ((),()))),(LinearOperators ((),()))) is set
K6(K7(K7((LinearOperators ((),())),(LinearOperators ((),()))),(LinearOperators ((),())))) is set
K198(K318( the carrier of (),()),(LinearOperators ((),()))) is Relation-like K7(REAL,(LinearOperators ((),()))) -defined LinearOperators ((),()) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(LinearOperators ((),()))),(LinearOperators ((),()))))
K7(REAL,(LinearOperators ((),()))) is set
K7(K7(REAL,(LinearOperators ((),()))),(LinearOperators ((),()))) is set
K6(K7(K7(REAL,(LinearOperators ((),()))),(LinearOperators ((),())))) is set
RLSStruct(# (LinearOperators ((),())),K199(K318( the carrier of (),()),(LinearOperators ((),()))),K197(K318( the carrier of (),()),(LinearOperators ((),()))),K198(K318( the carrier of (),()),(LinearOperators ((),()))) #) is V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of () is non empty set
K6( the carrier of ()) is set
K199((),(BoundedLinearOperators ((),()))) is Element of BoundedLinearOperators ((),())
K197((),(BoundedLinearOperators ((),()))) is Relation-like K7((BoundedLinearOperators ((),())),(BoundedLinearOperators ((),()))) -defined BoundedLinearOperators ((),()) -valued Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators ((),())),(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),()))))
K7((BoundedLinearOperators ((),())),(BoundedLinearOperators ((),()))) is set
K7(K7((BoundedLinearOperators ((),())),(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),()))) is set
K6(K7(K7((BoundedLinearOperators ((),())),(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),())))) is set
K198((),(BoundedLinearOperators ((),()))) is Relation-like K7(REAL,(BoundedLinearOperators ((),()))) -defined BoundedLinearOperators ((),()) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),()))))
K7(REAL,(BoundedLinearOperators ((),()))) is set
K7(K7(REAL,(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),()))) is set
K6(K7(K7(REAL,(BoundedLinearOperators ((),()))),(BoundedLinearOperators ((),())))) is set

K6(K7((BoundedLinearOperators ((),())),REAL)) is set
NORMSTR(# (BoundedLinearOperators ((),())),K199((),(BoundedLinearOperators ((),()))),K197((),(BoundedLinearOperators ((),()))),K198((),(BoundedLinearOperators ((),()))),(BoundedLinearOperatorsNorm ((),())) #) is strict NORMSTR
the carrier of () is non empty set

K6(K7(COMPLEX,COMPLEX)) is set

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

K6(K7(RAT,RAT)) is set

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

K6(K7(INT,INT)) is set

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

K6(K7(K7(NAT,NAT),NAT)) is set
K541() is non empty V73() L8()
the carrier of K541() is non empty set
K546() is non empty V73() V164() V165() V166() V168() V224() V225() V226() V227() V228() V229() L8()
K547() is non empty V73() V166() V168() V227() V228() V229() M17(K546())
K548() is non empty V73() V164() V166() V168() V227() V228() V229() V230() M20(K546(),K547())
K550() is non empty V73() V164() V166() V168() L8()
K551() is non empty V73() V164() V166() V168() V230() M17(K550())
ExtREAL is non empty ext-real-membered V263() set

{{},1} is non empty set
K310() is V94() L11()
the carrier of K310() is set
the carrier of K310() * is non empty functional FinSequence-membered FinSequenceSet of the carrier of K310()

K6(K7(COMPLEX,REAL)) is set

sqrt 1 is V11() real ext-real Element of REAL

K6(K7((REAL 1),REAL)) is set
(proj (1,1)) " is Relation-like Function-like set
K7(REAL,(REAL 1)) is set
K6(K7(REAL,(REAL 1))) is set
proj1 ((proj (1,1)) ") is set
proj2 ((proj (1,1)) ") is set

[1,1] is V27() set

{{1,1},{1}} is non empty set
{[1,1]} is non empty Function-like set

the carrier of () is non empty set

the carrier of () is non empty set
m is V11() real ext-real set
f is V11() real ext-real set

the carrier of () is non empty set

K38(1) is non empty V11() real ext-real non positive negative set

the carrier of () is non empty set

the carrier of m is non empty set
f is Element of the carrier of m
X is Neighbourhood of f
i is Neighbourhood of f
X /\ i is Element of K6( the carrier of m)
K6( the carrier of m) is set
y0 is Neighbourhood of f
r is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of m : not r <= ||.(b1 - f).|| } is set

f - m is V11() real ext-real V163() V198() Element of INT
(m + f) - m is V11() real ext-real V163() V198() Element of INT

{ } is set

{ } is set

K6(K7((Seg m),)) is set

{ } is set

{ } is set

K6(K7((Seg f),)) is set

{ } is set

{ } is set

K6(K7((Seg (f -' m)),)) is set

{ } is set
((0* m) ^ (0* (f -' m))) | (Seg (len (0* m))) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set

(m + f) - m is V11() real ext-real V163() V198() Element of INT

{ } is set

{ } is set

K6(K7((Seg (m -' 1)),)) is set

{ } is set

{ } is set

K6(K7((Seg f),)) is set

m - 1 is V11() real ext-real V163() V198() Element of INT
f - 1 is V11() real ext-real V163() V198() Element of INT

{ } is set

{ } is set

K6(K7((Seg f),)) is set

{ } is set

{ } is set

K6(K7((Seg (f -' m)),)) is set

((0* f) /^ m) . X is V11() real ext-real Element of REAL
(0* (f -' m)) . X is V11() real ext-real Element of REAL

(0* f) . (X + m) is V11() real ext-real Element of REAL

{ } is set

{ } is set

K6(K7((Seg f),)) is set

{ } is set

{ } is set

K6(K7((Seg (f -' m)),)) is set

f - m is V11() real ext-real V163() V198() Element of INT

{ } is set

{ } is set

K6(K7((Seg m),)) is set

{ } is set

{ } is set

K6(K7((Seg (m -' f)),)) is set

{ } is set

{ } is set

K6(K7((Seg f),)) is set

{ } is set

{ } is set

K6(K7((Seg (m -' 1)),)) is set

{ } is set

{ } is set

K6(K7((Seg i),)) is set

{ } is set

{ } is set

K6(K7((Seg (i -' X)),)) is set

the carrier of () is non empty set
0. () is V52( REAL-NS f) Element of the carrier of ()
reproj (m,(0. ())) is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total Element of K6(K7( the carrier of (), the carrier of ()))
K7( the carrier of (), the carrier of ()) is set
K6(K7( the carrier of (), the carrier of ())) is set
X is Element of the carrier of ()
(reproj (m,(0. ()))) . X is Element of the carrier of ()
||.((reproj (m,(0. ()))) . X).|| is V11() real ext-real Element of REAL
the U8 of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of (),REAL))
K7( the carrier of (),REAL) is complex-valued ext-real-valued real-valued set
K6(K7( the carrier of (),REAL)) is set
the U8 of () . ((reproj (m,(0. ()))) . X) is V11() real ext-real Element of REAL

the U8 of () is non empty Relation-like the carrier of () -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of (),REAL))
K7( the carrier of (),REAL) is complex-valued ext-real-valued real-valued set
K6(K7( the carrier of (),REAL)) is set
the U8 of () . X is V11() real ext-real Element of REAL

{ } is set
i is V11() real ext-real Element of REAL

[1,i] is V27() set

{{1,i},{1}} is non empty set
{[1,i]} is non empty Function-like set

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

{ } is set

|.(((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)).| is V11() real ext-real non negative Element of REAL

mlt ((((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)),(((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)))) is V11() real ext-real Element of REAL

{ } is set

K6(K7((Seg f),)) is set

Sum (sqr (y0 | (m -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (y0 | (m -' 1)))) is V11() real ext-real Element of REAL

{ } is set

K6(K7((Seg (m -' 1)),)) is set
|.(0* (m -' 1)).| is V11() real ext-real non negative Element of REAL

Sum (sqr (0* (m -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (0* (m -' 1)))) is V11() real ext-real Element of REAL

Sum (sqr (y0 /^ m)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL

{ } is set

{ } is set

K6(K7((Seg (f -' m)),)) is set
|.(0* (f -' m)).| is V11() real ext-real non negative Element of REAL

Sum (sqr (0* (f -' m))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (0* (f -' m)))) is V11() real ext-real Element of REAL

mlt (((y0 | (m -' 1)) ^ <*i*>),((y0 | (m -' 1)) ^ <*i*>)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

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

[1,(i ^2)] is V27() set

{{1,(i ^2)},{1}} is non empty set
{[1,(i ^2)]} is non empty Function-like set

((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>) ^ (sqr (y0 /^ m)) is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum ((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>) is V11() real ext-real Element of REAL
(Sum ((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>)) + (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL
(Sum (sqr (y0 | (m -' 1)))) + (i ^2) is V11() real ext-real Element of REAL
((Sum (sqr (y0 | (m -' 1)))) + (i ^2)) + (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL

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