:: NORMSP_1 semantic presentation

REAL is non empty V50() V124() V125() V126() V130() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() Element of bool REAL

COMPLEX is non empty V50() V124() V130() set
omega is non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() set

RAT is non empty V50() V124() V125() V126() V127() V130() set
INT is non empty V50() V124() V125() V126() V127() V128() V130() set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT

- 1 is ext-real non positive V36() real Element of REAL
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
[: the non empty set , the non empty set :] is set
[:[: the non empty set , the non empty set :], the non empty set :] is set
bool [:[: the non empty set , the non empty set :], the non empty set :] is set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:REAL, the non empty set :] is set
[:[:REAL, the non empty set :], the non empty set :] is set
bool [:[:REAL, the non empty set :], the non empty set :] is set
the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :] is Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :]
[: the non empty set ,REAL:] is set
bool [: the non empty set ,REAL:] is set
the Relation-like the non empty set -defined REAL -valued Function-like V18( the non empty set , REAL ) Element of bool [: the non empty set ,REAL:] is Relation-like the non empty set -defined REAL -valued Function-like V18( the non empty set , REAL ) Element of bool [: the non empty set ,REAL:]
( the non empty set , the Element of the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :], the Relation-like the non empty set -defined REAL -valued Function-like V18( the non empty set , REAL ) Element of bool [: the non empty set ,REAL:]) is () ()
the carrier of ( the non empty set , the Element of the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like V18([:REAL, the non empty set :], the non empty set ) Element of bool [:[:REAL, the non empty set :], the non empty set :], the Relation-like the non empty set -defined REAL -valued Function-like V18( the non empty set , REAL ) Element of bool [: the non empty set ,REAL:]) is set

the carrier of () is non empty set

[: the carrier of (),REAL:] is set
bool [: the carrier of (),REAL:] is set
the carrier of () --> 0 is Relation-like the carrier of () -defined NAT -valued Function-like V18( the carrier of (), NAT ) Element of bool [: the carrier of (),NAT:]
[: the carrier of (),NAT:] is set
bool [: the carrier of (),NAT:] is set
niltonil is Relation-like the carrier of () -defined REAL -valued Function-like V18( the carrier of (), REAL ) Element of bool [: the carrier of (),REAL:]
niltonil . () is set
X is left_complementable right_complementable complementable Element of the carrier of ()
niltonil . X is ext-real V36() real Element of REAL
a is ext-real V36() real Element of REAL
a * X is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (a,X) is set
niltonil . (a * X) is ext-real V36() real Element of REAL

(abs a) * (niltonil . X) is ext-real V36() real Element of REAL
X is left_complementable right_complementable complementable Element of the carrier of ()
a is left_complementable right_complementable complementable Element of the carrier of ()
X + a is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (X,a) is left_complementable right_complementable complementable Element of the carrier of ()
niltonil . (X + a) is ext-real V36() real Element of REAL
niltonil . X is ext-real V36() real Element of REAL
niltonil . a is ext-real V36() real Element of REAL
(niltonil . X) + (niltonil . a) is ext-real V36() real Element of REAL

the ZeroF of () is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V18([:REAL, the carrier of ():], the carrier of ()) Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
( the carrier of (),(0. ()), the addF of (), the Mult of (),niltonil) is () ()
X is non empty ()
the carrier of X is non empty set
a is Element of the carrier of X
RNS is Element of the carrier of X
0. X is V69(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X

the normF of X is Relation-like the carrier of X -defined REAL -valued Function-like V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
the normF of X . a is ext-real V36() real Element of REAL
S is ext-real V36() real Element of REAL
S * a is Element of the carrier of X
the Mult of X is Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V18([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is set
the Mult of X . (S,a) is set
g is left_complementable right_complementable complementable Element of the carrier of ()
S * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (S,g) is set
||.(S * a).|| is ext-real V36() real Element of REAL
the normF of X . (S * a) is ext-real V36() real Element of REAL

(abs S) * is ext-real V36() real Element of REAL
a + RNS is Element of the carrier of X
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
the addF of X . (a,RNS) is Element of the carrier of X
h is left_complementable right_complementable complementable Element of the carrier of ()
g + h is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (g,h) is left_complementable right_complementable complementable Element of the carrier of ()
||.(a + RNS).|| is ext-real V36() real Element of REAL
the normF of X . (a + RNS) is ext-real V36() real Element of REAL
||.RNS.|| is ext-real V36() real Element of REAL
the normF of X . RNS is ext-real V36() real Element of REAL
+ ||.RNS.|| is ext-real V36() real Element of REAL
||.(0. X).|| is ext-real V36() real Element of REAL
the normF of X . (0. X) is ext-real V36() real Element of REAL
a is ext-real V36() real set
RNS is Element of the carrier of X
S is Element of the carrier of X
RNS + S is Element of the carrier of X
the addF of X . (RNS,S) is Element of the carrier of X
a * (RNS + S) is Element of the carrier of X
the Mult of X . (a,(RNS + S)) is set
a * RNS is Element of the carrier of X
the Mult of X . (a,RNS) is set
a * S is Element of the carrier of X
the Mult of X . (a,S) is set
(a * RNS) + (a * S) is Element of the carrier of X
the addF of X . ((a * RNS),(a * S)) is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ()
h is left_complementable right_complementable complementable Element of the carrier of ()
g + h is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (g,h) is left_complementable right_complementable complementable Element of the carrier of ()
a * (g + h) is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (a,(g + h)) is set
a * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (a,g) is set
a * h is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (a,h) is set
(a * g) + (a * h) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . ((a * g),(a * h)) is left_complementable right_complementable complementable Element of the carrier of ()
a is ext-real V36() real set
RNS is ext-real V36() real set
a + RNS is ext-real V36() real set
S is Element of the carrier of X
(a + RNS) * S is Element of the carrier of X
the Mult of X . ((a + RNS),S) is set
a * S is Element of the carrier of X
the Mult of X . (a,S) is set
RNS * S is Element of the carrier of X
the Mult of X . (RNS,S) is set
(a * S) + (RNS * S) is Element of the carrier of X
the addF of X . ((a * S),(RNS * S)) is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ()
(a + RNS) * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . ((a + RNS),g) is set
a * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (a,g) is set
RNS * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (RNS,g) is set
(a * g) + (RNS * g) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . ((a * g),(RNS * g)) is left_complementable right_complementable complementable Element of the carrier of ()
a is ext-real V36() real set
RNS is ext-real V36() real set
a * RNS is ext-real V36() real set
S is Element of the carrier of X
(a * RNS) * S is Element of the carrier of X
the Mult of X . ((a * RNS),S) is set
RNS * S is Element of the carrier of X
the Mult of X . (RNS,S) is set
a * (RNS * S) is Element of the carrier of X
the Mult of X . (a,(RNS * S)) is set
g is left_complementable right_complementable complementable Element of the carrier of ()
(a * RNS) * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . ((a * RNS),g) is set
RNS * g is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (RNS,g) is set
a * (RNS * g) is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (a,(RNS * g)) is set
a is Element of the carrier of X
1 * a is Element of the carrier of X
the Mult of X . (1,a) is set
RNS is left_complementable right_complementable complementable Element of the carrier of ()
1 * RNS is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (1,RNS) is set
a is Element of the carrier of X
S is left_complementable right_complementable complementable Element of the carrier of ()
RNS is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ()
a + RNS is Element of the carrier of X
the addF of X . (a,RNS) is Element of the carrier of X
S + g is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (S,g) is left_complementable right_complementable complementable Element of the carrier of ()
h is ext-real V36() real Element of REAL
h * a is Element of the carrier of X
the Mult of X . (h,a) is set
h * S is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (h,S) is set
a is Element of the carrier of X
RNS is Element of the carrier of X
a + RNS is Element of the carrier of X
the addF of X . (a,RNS) is Element of the carrier of X
RNS + a is Element of the carrier of X
the addF of X . (RNS,a) is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ()
S is left_complementable right_complementable complementable Element of the carrier of ()
g + S is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (g,S) is left_complementable right_complementable complementable Element of the carrier of ()
a is Element of the carrier of X
RNS is Element of the carrier of X
a + RNS is Element of the carrier of X
the addF of X . (a,RNS) is Element of the carrier of X
S is Element of the carrier of X
(a + RNS) + S is Element of the carrier of X
the addF of X . ((a + RNS),S) is Element of the carrier of X
RNS + S is Element of the carrier of X
the addF of X . (RNS,S) is Element of the carrier of X
a + (RNS + S) is Element of the carrier of X
the addF of X . (a,(RNS + S)) is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ()
h is left_complementable right_complementable complementable Element of the carrier of ()
g + h is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (g,h) is left_complementable right_complementable complementable Element of the carrier of ()
r is left_complementable right_complementable complementable Element of the carrier of ()
(g + h) + r is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . ((g + h),r) is left_complementable right_complementable complementable Element of the carrier of ()
h + r is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (h,r) is left_complementable right_complementable complementable Element of the carrier of ()
g + (h + r) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (g,(h + r)) is left_complementable right_complementable complementable Element of the carrier of ()
a is Element of the carrier of X
a + (0. X) is Element of the carrier of X
the addF of X . (a,(0. X)) is Element of the carrier of X
RNS is left_complementable right_complementable complementable Element of the carrier of ()
RNS + (0. ()) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (RNS,(0. ())) is left_complementable right_complementable complementable Element of the carrier of ()
a is Element of the carrier of X
RNS is left_complementable right_complementable complementable Element of the carrier of ()
S is left_complementable right_complementable complementable Element of the carrier of ()
RNS + S is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . (RNS,S) is left_complementable right_complementable complementable Element of the carrier of ()
g is Element of the carrier of X
a + g is Element of the carrier of X
the addF of X . (a,g) is Element of the carrier of X

the carrier of a is non empty set
the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a

the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (0. a) is ext-real V36() real Element of REAL

the carrier of a is non empty set

||.(- RNS).|| is ext-real V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (- RNS) is ext-real V36() real Element of REAL
||.RNS.|| is ext-real V36() real Element of REAL
the normF of a . RNS is ext-real V36() real Element of REAL
abs (- 1) is ext-real V36() real Element of REAL
- (- 1) is ext-real non negative V36() real Element of REAL
(- 1) * RNS is left_complementable right_complementable complementable Element of the carrier of a
the Mult of a is Relation-like [:REAL, the carrier of a:] -defined the carrier of a -valued Function-like V18([:REAL, the carrier of a:], the carrier of a) Element of bool [:[:REAL, the carrier of a:], the carrier of a:]
[:REAL, the carrier of a:] is set
[:[:REAL, the carrier of a:], the carrier of a:] is set
bool [:[:REAL, the carrier of a:], the carrier of a:] is set
the Mult of a . ((- 1),RNS) is set
||.((- 1) * RNS).|| is ext-real V36() real Element of REAL
the normF of a . ((- 1) * RNS) is ext-real V36() real Element of REAL
(abs (- 1)) * ||.RNS.|| is ext-real V36() real Element of REAL

the carrier of a is non empty set

||.RNS.|| is ext-real V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . RNS is ext-real V36() real Element of REAL

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real V36() real Element of REAL
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

the normF of a . S is ext-real V36() real Element of REAL
||.RNS.|| + is ext-real V36() real Element of REAL
||.(- S).|| is ext-real V36() real Element of REAL
the normF of a . (- S) is ext-real V36() real Element of REAL
||.RNS.|| + ||.(- S).|| is ext-real V36() real Element of REAL

the carrier of a is non empty set

||.RNS.|| is ext-real V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . RNS is ext-real V36() real Element of REAL
RNS - RNS is left_complementable right_complementable complementable Element of the carrier of a

RNS + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - RNS).|| is ext-real V36() real Element of REAL
the normF of a . (RNS - RNS) is ext-real V36() real Element of REAL

the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a

the normF of a . (0. a) is ext-real V36() real Element of REAL
||.RNS.|| + ||.RNS.|| is ext-real V36() real Element of REAL
(||.RNS.|| + ||.RNS.||) / 2 is ext-real V36() real Element of REAL

the carrier of a is non empty set

||.RNS.|| is ext-real V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . RNS is ext-real V36() real Element of REAL
a is ext-real V36() real Element of REAL

RNS is ext-real V36() real Element of REAL
abs RNS is ext-real V36() real Element of REAL

the carrier of S is non empty set

the Mult of S is Relation-like [:REAL, the carrier of S:] -defined the carrier of S -valued Function-like V18([:REAL, the carrier of S:], the carrier of S) Element of bool [:[:REAL, the carrier of S:], the carrier of S:]
[:REAL, the carrier of S:] is set
[:[:REAL, the carrier of S:], the carrier of S:] is set
bool [:[:REAL, the carrier of S:], the carrier of S:] is set
the Mult of S . (a,g) is set
is ext-real non negative V36() real Element of REAL
the normF of S is Relation-like the carrier of S -defined REAL -valued Function-like V18( the carrier of S, REAL ) Element of bool [: the carrier of S,REAL:]
[: the carrier of S,REAL:] is set
bool [: the carrier of S,REAL:] is set
the normF of S . g is ext-real V36() real Element of REAL
(abs a) * is ext-real V36() real Element of REAL

the Mult of S . (RNS,h) is set
(a * g) + (RNS * h) is left_complementable right_complementable complementable Element of the carrier of S
the addF of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is set
the addF of S . ((a * g),(RNS * h)) is left_complementable right_complementable complementable Element of the carrier of S
||.((a * g) + (RNS * h)).|| is ext-real non negative V36() real Element of REAL
the normF of S . ((a * g) + (RNS * h)) is ext-real V36() real Element of REAL
is ext-real non negative V36() real Element of REAL
the normF of S . h is ext-real V36() real Element of REAL
(abs RNS) * is ext-real V36() real Element of REAL
((abs a) * ) + ((abs RNS) * ) is ext-real V36() real Element of REAL
||.(a * g).|| is ext-real non negative V36() real Element of REAL
the normF of S . (a * g) is ext-real V36() real Element of REAL
||.(RNS * h).|| is ext-real non negative V36() real Element of REAL
the normF of S . (RNS * h) is ext-real V36() real Element of REAL
||.(a * g).|| + ||.(RNS * h).|| is ext-real non negative V36() real Element of REAL
((abs a) * ) + ||.(RNS * h).|| is ext-real V36() real Element of REAL

the carrier of a is non empty set

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a

the carrier of a is non empty set

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

S + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
||.(S - RNS).|| is ext-real non negative V36() real Element of REAL
the normF of a . (S - RNS) is ext-real V36() real Element of REAL
- (S - RNS) is left_complementable right_complementable complementable Element of the carrier of a

the carrier of a is non empty set

||.RNS.|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . RNS is ext-real V36() real Element of REAL

is ext-real non negative V36() real Element of REAL
the normF of a . S is ext-real V36() real Element of REAL
||.RNS.|| - is ext-real V36() real Element of REAL

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a . (RNS - S) is ext-real V36() real Element of REAL
(RNS - S) + S is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((RNS - S),S) is left_complementable right_complementable complementable Element of the carrier of a

the addF of a . (S,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
RNS - (S - S) is left_complementable right_complementable complementable Element of the carrier of a
- (S - S) is left_complementable right_complementable complementable Element of the carrier of a
RNS + (- (S - S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(- (S - S))) is left_complementable right_complementable complementable Element of the carrier of a

the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a
RNS - H1(a) is left_complementable right_complementable complementable Element of the carrier of a

RNS + (- (0. a)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(- (0. a))) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| + is ext-real non negative V36() real Element of REAL

the carrier of a is non empty set

||.RNS.|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . RNS is ext-real V36() real Element of REAL

is ext-real non negative V36() real Element of REAL
the normF of a . S is ext-real V36() real Element of REAL
||.RNS.|| - is ext-real V36() real Element of REAL
abs (||.RNS.|| - ) is ext-real V36() real Element of REAL

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

S + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
(S - RNS) + RNS is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((S - RNS),RNS) is left_complementable right_complementable complementable Element of the carrier of a
RNS - RNS is left_complementable right_complementable complementable Element of the carrier of a
RNS + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
S - (RNS - RNS) is left_complementable right_complementable complementable Element of the carrier of a
- (RNS - RNS) is left_complementable right_complementable complementable Element of the carrier of a
S + (- (RNS - RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- (RNS - RNS))) is left_complementable right_complementable complementable Element of the carrier of a

the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a
S - H1(a) is left_complementable right_complementable complementable Element of the carrier of a

S + (- (0. a)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- (0. a))) is left_complementable right_complementable complementable Element of the carrier of a
||.(S - RNS).|| is ext-real non negative V36() real Element of REAL
the normF of a . (S - RNS) is ext-real V36() real Element of REAL
||.(S - RNS).|| + ||.RNS.|| is ext-real non negative V36() real Element of REAL
- ||.RNS.|| is ext-real V36() real Element of REAL
- ||.(RNS - S).|| is ext-real non positive V36() real Element of REAL
- ( - ||.RNS.||) is ext-real V36() real Element of REAL

the carrier of a is non empty set

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

RNS + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . (RNS - g) is ext-real V36() real Element of REAL

the addF of a . (g,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(g - S).|| is ext-real non negative V36() real Element of REAL
the normF of a . (g - S) is ext-real V36() real Element of REAL
||.(RNS - g).|| + ||.(g - S).|| is ext-real non negative V36() real Element of REAL

the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a
H1(a) + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((0. a),(- S)) is left_complementable right_complementable complementable Element of the carrier of a
RNS + (H1(a) + (- S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(H1(a) + (- S))) is left_complementable right_complementable complementable Element of the carrier of a

the addF of a . ((- g),g) is left_complementable right_complementable complementable Element of the carrier of a
((- g) + g) + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((- g) + g),(- S)) is left_complementable right_complementable complementable Element of the carrier of a
RNS + (((- g) + g) + (- S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,(((- g) + g) + (- S))) is left_complementable right_complementable complementable Element of the carrier of a

(- g) + (g + (- S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- g),(g + (- S))) is left_complementable right_complementable complementable Element of the carrier of a
RNS + ((- g) + (g + (- S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (RNS,((- g) + (g + (- S)))) is left_complementable right_complementable complementable Element of the carrier of a
(RNS - g) + (g - S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((RNS - g),(g - S)) is left_complementable right_complementable complementable Element of the carrier of a

the carrier of a is non empty set

RNS + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (RNS,(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(RNS - S).|| is ext-real non negative V36() real Element of REAL
the normF of a is Relation-like the carrier of a -defined REAL -valued Function-like V18( the carrier of a, REAL ) Element of bool [: the carrier of a,REAL:]
[: the carrier of a,REAL:] is set
bool [: the carrier of a,REAL:] is set
the normF of a . (RNS - S) is ext-real V36() real Element of REAL

dom a is set
RNS is non empty 1-sorted
the carrier of RNS is non empty set
[:NAT, the carrier of RNS:] is set
bool [:NAT, the carrier of RNS:] is set
rng a is set
g is set
a . g is set
g is set
a . g is set
rng a is set
g is set
h is set
a . h is set
a is non empty 1-sorted
the carrier of a is non empty set
[:NAT, the carrier of a:] is set
bool [:NAT, the carrier of a:] is set
RNS is Element of the carrier of a
{RNS} is non empty Element of bool the carrier of a
bool the carrier of a is set

dom S is set
rng S is set
g is Relation-like NAT -defined the carrier of a -valued Function-like V18( NAT , the carrier of a) Element of bool [:NAT, the carrier of a:]
rng g is set
a is non empty 1-sorted
the carrier of a is non empty set
[:NAT, the carrier of a:] is set
bool [:NAT, the carrier of a:] is set
RNS is Relation-like NAT -defined the carrier of a -valued Function-like V18( NAT , the carrier of a) Element of bool [:NAT, the carrier of a:]
rng RNS is set
S is Element of the carrier of a
g is Element of the carrier of a
{g} is non empty Element of bool the carrier of a
bool the carrier of a is set
h is set

dom RNS is set
RNS . r is Element of the carrier of a
h is set
r is set