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
bool REAL is set
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
bool omega is set
bool NAT is set
RAT is non empty V50() V124() V125() V126() V127() V130() set
INT is non empty V50() V124() V125() V126() V127() V128() V130() set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() 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
0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() 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 non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct
(0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() Subspace of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct
the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is non empty set
the carrier of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is non empty set
0. the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is V69( the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) left_complementable right_complementable complementable Element of the carrier of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct
the ZeroF of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is left_complementable right_complementable complementable Element of the carrier of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct
{(0. the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )} is non empty Element of bool the carrier of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct
bool the carrier of the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct is set
[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),REAL:] is set
bool [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),REAL:] is set
the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) --> 0 is Relation-like the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -defined NAT -valued Function-like V18( the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), NAT ) Element of bool [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),NAT:]
[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),NAT:] is set
bool [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),NAT:] is set
niltonil is Relation-like the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -defined REAL -valued Function-like V18( the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), REAL ) Element of bool [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),REAL:]
niltonil . (0. the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is set
X is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is Relation-like [:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] -defined the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -valued Function-like V18([:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )) Element of bool [:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):]
[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
[:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
bool [:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (a,X) is set
niltonil . (a * X) is ext-real V36() real Element of REAL
abs a 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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
a is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
X + a is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is Relation-like [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] -defined the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -valued Function-like V18([: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )) Element of bool [:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):]
[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
[:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
bool [:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (X,a) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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
0. ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is V69( (0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the ZeroF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is Relation-like [: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] -defined the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -valued Function-like V18([: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )) Element of bool [:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):]
[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
[:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
bool [:[: the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) is Relation-like [:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] -defined the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) -valued Function-like V18([:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )) Element of bool [:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):]
[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
[:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
bool [:[:REAL, the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):], the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ):] is set
( the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),(0. ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )), the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ), the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ),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
||.a.|| is ext-real V36() real Element of REAL
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
S * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (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
(abs S) * ||.a.|| 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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
g + h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (g,h) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
||.(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
||.a.|| + ||.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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
g + h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (g,h) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
a * (g + h) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (a,(g + h)) is set
a * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (a,g) is set
a * h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (a,h) is set
(a * g) + (a * h) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . ((a * g),(a * h)) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
(a + RNS) * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . ((a + RNS),g) is set
a * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (a,g) is set
RNS * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (RNS,g) is set
(a * g) + (RNS * g) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . ((a * g),(RNS * g)) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
(a * RNS) * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . ((a * RNS),g) is set
RNS * g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (RNS,g) is set
a * (RNS * g) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
1 * RNS is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (1,RNS) is set
a is Element of the carrier of X
S is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
RNS is Element of the carrier of X
g is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (S,g) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the Mult of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
S is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
g + S is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (g,S) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
g + h is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (g,h) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
r is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
(g + h) + r is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . ((g + h),r) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
h + r is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (h,r) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
g + (h + r) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (g,(h + r)) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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 ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
RNS + (0. ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (RNS,(0. ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ))) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
a is Element of the carrier of X
RNS is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
S is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
RNS + S is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
the addF of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct ) . (RNS,S) is left_complementable right_complementable complementable Element of the carrier of ((0). the non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() RLSStruct )
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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
0. a is V69(a) left_complementable right_complementable complementable Element of the carrier of a
the carrier of a is non empty set
the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a
||.(0. a).|| is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() 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 . (0. a) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
- RNS is left_complementable right_complementable complementable Element of the carrier of a
||.(- 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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
||.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
S is left_complementable right_complementable complementable Element of the carrier of a
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
||.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
||.(- 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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
||.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 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
0. a is V69(a) 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
||.H1(a).|| is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() Element of REAL
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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
||.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
abs 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
S is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of S is non empty set
g is left_complementable right_complementable complementable Element of the carrier of S
a * g is left_complementable right_complementable complementable Element of the carrier of S
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
||.g.|| 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) * ||.g.|| is ext-real V36() real Element of REAL
h is left_complementable right_complementable complementable Element of the carrier of S
RNS * h is left_complementable right_complementable complementable Element of the carrier of S
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
||.h.|| 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) * ||.h.|| is ext-real V36() real Element of REAL
((abs a) * ||.g.||) + ((abs RNS) * ||.h.||) 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) * ||.g.||) + ||.(RNS * h).|| is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
S is left_complementable right_complementable complementable Element of the carrier of a
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
0. a is V69(a) 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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
S is left_complementable right_complementable complementable Element of the carrier of a
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
- RNS is left_complementable right_complementable complementable Element of the carrier of a
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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
||.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
S is left_complementable right_complementable complementable Element of the carrier of a
||.S.|| is ext-real non negative 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
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
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
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
0. a is V69(a) 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
- (0. 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).|| + ||.S.|| is ext-real non negative V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
||.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
S is left_complementable right_complementable complementable Element of the carrier of a
||.S.|| is ext-real non negative 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
abs (||.RNS.|| - ||.S.||) is ext-real V36() real Element of REAL
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
- RNS is left_complementable right_complementable complementable Element of the carrier of a
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
0. a is V69(a) 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
- (0. 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
||.S.|| - ||.RNS.|| is ext-real V36() real Element of REAL
- ||.(RNS - S).|| is ext-real non positive V36() real Element of REAL
- (||.S.|| - ||.RNS.||) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
S is left_complementable right_complementable complementable Element of the carrier of a
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
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 a
- 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 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
g - S is left_complementable right_complementable complementable Element of the carrier of a
g + (- S) is left_complementable right_complementable complementable Element of the carrier of a
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
0. a is V69(a) 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
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
(- g) + g 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 + (- 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
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
RNS is left_complementable right_complementable complementable Element of the carrier of a
S is left_complementable right_complementable complementable Element of the carrier of a
RNS - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
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
a is Relation-like Function-like set
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
S is Relation-like Function-like 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
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
dom RNS is set
RNS . r is Element of the carrier of a
h is set
r is set
RNS . r 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
{S} is non empty Element of bool the carrier of a
bool the carrier of a is set
g is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . g is Element of the carrier of a
g + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . (g + 1) is Element of the carrier of a
dom RNS 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:]
S is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . S is Element of the carrier of a
g is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
S + g is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . (S + g) is Element of the carrier of a
(S + g) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . ((S + g) + 1) is Element of the carrier of a
g + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
S + (g + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . (S + (g + 1)) is Element of the carrier of a
S + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . (S + 0) is Element of the carrier of a
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:]
S is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . S is Element of the carrier of a
g is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . g is Element of the carrier of a
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real set
g + h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
g + r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real set
S + h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
S + r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
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:]
S is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . S is Element of the carrier of a
g is Element of the carrier of a
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real set
RNS . 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 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:]
S is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . S is Element of the carrier of a
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:]
S is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
RNS . S is set
a is non empty addLoopStr
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:]
S 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:]
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:]
h 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:]
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,g,r) is Element of the carrier of a
(a,h,r) is Element of the carrier of a
(a,RNS,r) is Element of the carrier of a
(a,S,r) is Element of the carrier of a
(a,RNS,r) + (a,S,r) is 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 . ((a,RNS,r),(a,S,r)) is Element of the carrier of a
a is non empty addLoopStr
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:]
S 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:]
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:]
h 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:]
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,g,r) is Element of the carrier of a
(a,h,r) is Element of the carrier of a
(a,RNS,r) is Element of the carrier of a
(a,S,r) is Element of the carrier of a
(a,RNS,r) - (a,S,r) is Element of the carrier of a
- (a,S,r) is Element of the carrier of a
(a,RNS,r) + (- (a,S,r)) is 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 . ((a,RNS,r),(- (a,S,r))) is Element of the carrier of a
a is non empty addLoopStr
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:]
S is Element of the carrier of a
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:]
h 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:]
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,g,r) is Element of the carrier of a
(a,h,r) is Element of the carrier of a
(a,RNS,r) is Element of the carrier of a
(a,RNS,r) - S is Element of the carrier of a
- S is Element of the carrier of a
(a,RNS,r) + (- S) is 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 . ((a,RNS,r),(- S)) is Element of the carrier of a
a is non empty RLSStruct
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:]
S is ext-real V36() real Element of REAL
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:]
h 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:]
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,g,r) is Element of the carrier of a
(a,h,r) is Element of the carrier of a
(a,RNS,r) is Element of the carrier of a
S * (a,RNS,r) is 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 . (S,(a,RNS,r)) is set
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of a is non empty set
[:NAT, the carrier of a:] is set
bool [:NAT, the carrier of a:] is set
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
S 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:]
(a,RNS,S) 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:]
g is left_complementable right_complementable complementable Element of the carrier of a
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 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 . (g,h) is left_complementable right_complementable complementable Element of the carrier of a
r is left_complementable right_complementable complementable Element of the carrier of a
m1 is ext-real V36() real Element of REAL
m1 / 2 is ext-real V36() real Element of REAL
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k + n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,(a,RNS,S),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) - r is left_complementable right_complementable complementable Element of the carrier of a
- r is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) + (- r) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,RNS,S),n),(- r)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,RNS,S),n) - r).|| 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 . ((a,(a,RNS,S),n) - r) is ext-real V36() real Element of REAL
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - h is left_complementable right_complementable complementable Element of the carrier of a
- h is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - h).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,S,n) - h) is ext-real V36() real Element of REAL
- (g + h) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(- (g + h)) + ((a,RNS,n) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- (g + h)),((a,RNS,n) + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
||.((- (g + h)) + ((a,RNS,n) + (a,S,n))).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((- (g + h)) + ((a,RNS,n) + (a,S,n))) is ext-real V36() real Element of REAL
- g 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 a
the addF of a . ((- g),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
((- g) + (- h)) + ((a,RNS,n) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((- g) + (- h)),((a,RNS,n) + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((- g) + (- h)) + ((a,RNS,n) + (a,S,n))).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((- g) + (- h)) + ((a,RNS,n) + (a,S,n))) is ext-real V36() real Element of REAL
(a,RNS,n) + ((- g) + (- h)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),((- g) + (- h))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) + ((- g) + (- h))) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) + ((- g) + (- h))),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) + ((- g) + (- h))) + (a,S,n)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) + ((- g) + (- h))) + (a,S,n)) is ext-real V36() real Element of REAL
(a,RNS,n) - g is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - g) + (- h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - g),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - g) + (- h)) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - g) + (- h)),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - g) + (- h)) + (a,S,n)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - g) + (- h)) + (a,S,n)) is ext-real V36() real Element of REAL
((a,RNS,n) - g) + ((a,S,n) - h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - g),((a,S,n) - h)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - g) + ((a,S,n) - h)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - g) + ((a,S,n) - h)) is ext-real V36() real Element of REAL
||.((a,RNS,n) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,n) - g) is ext-real V36() real Element of REAL
||.((a,RNS,n) - g).|| + ||.((a,S,n) - h).|| is ext-real non negative V36() real Element of REAL
(m1 / 2) + (m1 / 2) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
S 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:]
(a,RNS,S) 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:]
g is left_complementable right_complementable complementable Element of the carrier of a
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 a
- 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 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 . (g,(- h)) is left_complementable right_complementable complementable Element of the carrier of a
r is left_complementable right_complementable complementable Element of the carrier of a
m1 is ext-real V36() real Element of REAL
m1 / 2 is ext-real V36() real Element of REAL
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k + n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,(a,RNS,S),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) - r is left_complementable right_complementable complementable Element of the carrier of a
- r is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) + (- r) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,RNS,S),n),(- r)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,RNS,S),n) - r).|| 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 . ((a,(a,RNS,S),n) - r) is ext-real V36() real Element of REAL
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - h is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - h).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,S,n) - h) is ext-real V36() real Element of REAL
(a,RNS,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) - (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
- (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,S,n)) - (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 a
((a,RNS,n) - (a,S,n)) + (- (g - h)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,S,n)),(- (g - h))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - (a,S,n)) - (g - h)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - (a,S,n)) - (g - h)) is ext-real V36() real Element of REAL
((a,RNS,n) - (a,S,n)) - g is left_complementable right_complementable complementable Element of the carrier of a
- g is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,S,n)) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,S,n)),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - (a,S,n)) - g) + h is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - (a,S,n)) - g),h) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - (a,S,n)) - g) + h).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - (a,S,n)) - g) + h) is ext-real V36() real Element of REAL
g + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (g,(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) - (g + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
- (g + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- (g + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- (g + (a,S,n)))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (g + (a,S,n))) + h is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (g + (a,S,n))),h) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - (g + (a,S,n))) + h).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - (g + (a,S,n))) + h) is ext-real V36() real Element of REAL
(a,RNS,n) - g is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - g) - (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - g) + (- (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - g),(- (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - g) - (a,S,n)) + h is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - g) - (a,S,n)),h) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - g) - (a,S,n)) + h).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - g) - (a,S,n)) + h) is ext-real V36() real Element of REAL
((a,RNS,n) - g) - ((a,S,n) - h) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,S,n) - h) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - g) + (- ((a,S,n) - h)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - g),(- ((a,S,n) - h))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - g) - ((a,S,n) - h)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - g) - ((a,S,n) - h)) is ext-real V36() real Element of REAL
||.((a,RNS,n) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,n) - g) is ext-real V36() real Element of REAL
||.((a,RNS,n) - g).|| + ||.((a,S,n) - h).|| is ext-real non negative V36() real Element of REAL
(m1 / 2) + (m1 / 2) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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 left_complementable right_complementable complementable Element of the carrier of a
S 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:]
(a,S,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:]
g is left_complementable right_complementable complementable Element of the carrier of a
g - RNS is left_complementable right_complementable complementable Element of the carrier of a
- RNS is left_complementable right_complementable complementable Element of the carrier of a
g + (- 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 . (g,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
h is left_complementable right_complementable complementable Element of the carrier of a
r is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,(a,S,RNS),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,S,RNS),n) - h is left_complementable right_complementable complementable Element of the carrier of a
- h is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,S,RNS),n) + (- h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,S,RNS),n),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,S,RNS),n) - h).|| 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 . ((a,(a,S,RNS),n) - h) is ext-real V36() real Element of REAL
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - g is left_complementable right_complementable complementable Element of the carrier of a
- g is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,S,n) - g) is ext-real V36() real Element of REAL
0. a is V69(a) 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
(a,S,n) - H1(a) is left_complementable right_complementable complementable Element of the carrier of a
- (0. a) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- (0. a)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (0. a))) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - H1(a)) - g is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - H1(a)) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - H1(a)),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - H1(a)) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - H1(a)) - g) 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 . (RNS,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - (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
(a,S,n) + (- (RNS - RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (RNS - RNS))) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - (RNS - RNS)) - g is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - (RNS - RNS)) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - (RNS - RNS)),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - (RNS - RNS)) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - (RNS - RNS)) - g) is ext-real V36() real Element of REAL
(a,S,n) - RNS is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + RNS is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),RNS) is left_complementable right_complementable complementable Element of the carrier of a
(((a,S,n) - RNS) + RNS) - g is left_complementable right_complementable complementable Element of the carrier of a
(((a,S,n) - RNS) + RNS) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,S,n) - RNS) + RNS),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,S,n) - RNS) + RNS) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,S,n) - RNS) + RNS) - g) is ext-real V36() real Element of REAL
(- g) + RNS is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- g),RNS) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + ((- g) + RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),((- g) + RNS)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - RNS) + ((- g) + RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - RNS) + ((- g) + RNS)) is ext-real V36() real Element of REAL
((a,S,n) - RNS) - h is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + (- h) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),(- h)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - RNS) - h).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - RNS) - h) is ext-real V36() real Element of REAL
a is ext-real V36() real Element of REAL
RNS is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of RNS is non empty set
[:NAT, the carrier of RNS:] is set
bool [:NAT, the carrier of RNS:] is set
S is Relation-like NAT -defined the carrier of RNS -valued Function-like V18( NAT , the carrier of RNS) Element of bool [:NAT, the carrier of RNS:]
(RNS,S,a) is Relation-like NAT -defined the carrier of RNS -valued Function-like V18( NAT , the carrier of RNS) Element of bool [:NAT, the carrier of RNS:]
g is left_complementable right_complementable complementable Element of the carrier of RNS
a * g is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS is Relation-like [:REAL, the carrier of RNS:] -defined the carrier of RNS -valued Function-like V18([:REAL, the carrier of RNS:], the carrier of RNS) Element of bool [:[:REAL, the carrier of RNS:], the carrier of RNS:]
[:REAL, the carrier of RNS:] is set
[:[:REAL, the carrier of RNS:], the carrier of RNS:] is set
bool [:[:REAL, the carrier of RNS:], the carrier of RNS:] is set
the Mult of RNS . (a,g) is set
h is left_complementable right_complementable complementable Element of the carrier of RNS
abs a is ext-real V36() real Element of REAL
0 / (abs a) is ext-real V36() real Element of REAL
r is ext-real V36() real Element of REAL
r / (abs a) is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) - g is left_complementable right_complementable complementable Element of the carrier of RNS
- g is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) + (- g) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS is Relation-like [: the carrier of RNS, the carrier of RNS:] -defined the carrier of RNS -valued Function-like V18([: the carrier of RNS, the carrier of RNS:], the carrier of RNS) Element of bool [:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:]
[: the carrier of RNS, the carrier of RNS:] is set
[:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:] is set
bool [:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:] is set
the addF of RNS . ((RNS,S,n),(- g)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,S,n) - g).|| is ext-real non negative V36() real Element of REAL
the normF of RNS is Relation-like the carrier of RNS -defined REAL -valued Function-like V18( the carrier of RNS, REAL ) Element of bool [: the carrier of RNS,REAL:]
[: the carrier of RNS,REAL:] is set
bool [: the carrier of RNS,REAL:] is set
the normF of RNS . ((RNS,S,n) - g) is ext-real V36() real Element of REAL
(abs a) * (r / (abs a)) is ext-real V36() real Element of REAL
(abs a) " is ext-real V36() real Element of REAL
((abs a) ") * r is ext-real V36() real Element of REAL
(abs a) * (((abs a) ") * r) is ext-real V36() real Element of REAL
(abs a) * ((abs a) ") is ext-real V36() real Element of REAL
((abs a) * ((abs a) ")) * r is ext-real V36() real Element of REAL
1 * r is ext-real V36() real Element of REAL
a * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,(RNS,S,n)) is set
(a * (RNS,S,n)) - (a * g) is left_complementable right_complementable complementable Element of the carrier of RNS
- (a * g) is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- (a * g)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- (a * g))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - (a * g)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - (a * g)) is ext-real V36() real Element of REAL
a * ((RNS,S,n) - g) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,((RNS,S,n) - g)) is set
||.(a * ((RNS,S,n) - g)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . (a * ((RNS,S,n) - g)) is ext-real V36() real Element of REAL
(abs a) * ||.((RNS,S,n) - g).|| is ext-real V36() real Element of REAL
(a * (RNS,S,n)) - h is left_complementable right_complementable complementable Element of the carrier of RNS
- h is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- h) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- h)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - h).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - h) is ext-real V36() real Element of REAL
(RNS,(RNS,S,a),n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) - h is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) + (- h) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,(RNS,S,a),n),(- h)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,(RNS,S,a),n) - h).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,(RNS,S,a),n) - h) is ext-real V36() real Element of REAL
r is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) - g is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) + (- g) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,S,n),(- g)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,S,n) - g).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,S,n) - g) is ext-real V36() real Element of REAL
a * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,(RNS,S,n)) is set
(a * (RNS,S,n)) - (a * g) is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- (a * g)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- (a * g))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - (a * g)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - (a * g)) is ext-real V36() real Element of REAL
0 * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (0,(RNS,S,n)) is set
0. RNS is V69(RNS) left_complementable right_complementable complementable Element of the carrier of RNS
the ZeroF of RNS is left_complementable right_complementable complementable Element of the carrier of RNS
(0 * (RNS,S,n)) - H1(RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
- (0. RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
(0 * (RNS,S,n)) + (- (0. RNS)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((0 * (RNS,S,n)),(- (0. RNS))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((0 * (RNS,S,n)) - H1(RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((0 * (RNS,S,n)) - H1(RNS)) is ext-real V36() real Element of REAL
H1(RNS) - H1(RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
(0. RNS) + (- (0. RNS)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((0. RNS),(- (0. RNS))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.(H1(RNS) - H1(RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . (H1(RNS) - H1(RNS)) is ext-real V36() real Element of REAL
||.H1(RNS).|| is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() Element of REAL
the normF of RNS . (0. RNS) is ext-real V36() real Element of REAL
(a * (RNS,S,n)) - h is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- h) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- h)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - h).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - h) is ext-real V36() real Element of REAL
(RNS,(RNS,S,a),n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) - h is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) + (- h) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,(RNS,S,a),n),(- h)) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,(RNS,S,a),n) - h).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,(RNS,S,a),n) - h) is ext-real V36() real Element of REAL
r is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
||.RNS.|| is Relation-like NAT -defined REAL -valued Function-like V18( NAT , REAL ) Element of bool [:NAT,REAL:]
S is left_complementable right_complementable complementable Element of the carrier of a
g is ext-real V36() real set
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,RNS,m1) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,m1) - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,m1) + (- 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 . ((a,RNS,m1),(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,RNS,m1) - 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 . ((a,RNS,m1) - S) is ext-real V36() real Element of REAL
||.(a,RNS,m1).|| is ext-real non negative V36() real Element of REAL
the normF of a . (a,RNS,m1) is ext-real V36() real Element of REAL
||.S.|| is ext-real non negative V36() real Element of REAL
the normF of a . S is ext-real V36() real Element of REAL
||.(a,RNS,m1).|| - ||.S.|| is ext-real V36() real Element of REAL
abs (||.(a,RNS,m1).|| - ||.S.||) is ext-real V36() real Element of REAL
||.RNS.|| . m1 is ext-real V36() real Element of REAL
(||.RNS.|| . m1) - ||.S.|| is ext-real V36() real Element of REAL
abs ((||.RNS.|| . m1) - ||.S.||) is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
||.RNS.|| . m1 is ext-real V36() real Element of REAL
(||.RNS.|| . m1) - ||.S.|| is ext-real V36() real Element of REAL
abs ((||.RNS.|| . m1) - ||.S.||) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
S is left_complementable right_complementable complementable Element of the carrier of a
g is left_complementable right_complementable complementable Element of the carrier of a
S - g is left_complementable right_complementable complementable Element of the carrier of a
- g is left_complementable right_complementable complementable Element of the carrier of a
S + (- g) 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 . (S,(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.(S - g).|| 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 . (S - g) is ext-real V36() real Element of REAL
4 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
||.(S - g).|| / 4 is ext-real non negative V36() real Element of REAL
0 / 4 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() Element of REAL
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,RNS,h) is left_complementable right_complementable complementable Element of the carrier of a
S - (a,RNS,h) is left_complementable right_complementable complementable Element of the carrier of a
- (a,RNS,h) is left_complementable right_complementable complementable Element of the carrier of a
S + (- (a,RNS,h)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- (a,RNS,h))) is left_complementable right_complementable complementable Element of the carrier of a
||.(S - (a,RNS,h)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (S - (a,RNS,h)) is ext-real V36() real Element of REAL
(a,RNS,h) - g is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,h) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,h),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,RNS,h) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,h) - g) is ext-real V36() real Element of REAL
||.(S - (a,RNS,h)).|| + ||.((a,RNS,h) - g).|| is ext-real non negative V36() real Element of REAL
(a,RNS,h) - S is left_complementable right_complementable complementable Element of the carrier of a
- S is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,h) + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,h),(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,RNS,h) - S).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,h) - S) is ext-real V36() real Element of REAL
||.((a,RNS,h) - S).|| + ||.((a,RNS,h) - g).|| is ext-real non negative V36() real Element of REAL
(||.(S - g).|| / 4) + (||.(S - g).|| / 4) is ext-real non negative V36() real Element of REAL
||.(S - g).|| / 2 is ext-real non negative V36() real Element of REAL
(a,RNS,r) is left_complementable right_complementable complementable Element of the carrier of a
S - (a,RNS,r) is left_complementable right_complementable complementable Element of the carrier of a
- (a,RNS,r) is left_complementable right_complementable complementable Element of the carrier of a
S + (- (a,RNS,r)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (S,(- (a,RNS,r))) is left_complementable right_complementable complementable Element of the carrier of a
||.(S - (a,RNS,r)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (S - (a,RNS,r)) is ext-real V36() real Element of REAL
(a,RNS,r) - g is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,r) + (- g) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,r),(- g)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,RNS,r) - g).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,r) - g) is ext-real V36() real Element of REAL
||.(S - (a,RNS,r)).|| + ||.((a,RNS,r) - g).|| is ext-real non negative V36() real Element of REAL
(a,RNS,r) - S is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,r) + (- S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,r),(- S)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,RNS,r) - S).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,r) - S) is ext-real V36() real Element of REAL
||.((a,RNS,r) - S).|| + ||.((a,RNS,r) - g).|| is ext-real non negative V36() real Element of REAL
S is left_complementable right_complementable complementable Element of the carrier of a
g is left_complementable right_complementable complementable Element of the carrier of a
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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 left_complementable right_complementable complementable Element of the carrier of a
S 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:]
(a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,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:]
||.(a,S,RNS).|| is Relation-like NAT -defined REAL -valued Function-like V18( NAT , REAL ) Element of bool [:NAT,REAL:]
lim ||.(a,S,RNS).|| is ext-real V36() real Element of REAL
g is ext-real V36() real set
h is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
r is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,S,m1) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,m1) - RNS is left_complementable right_complementable complementable Element of the carrier of a
- RNS is left_complementable right_complementable complementable Element of the carrier of a
(a,S,m1) + (- 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 . ((a,S,m1),(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,m1) - 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 . ((a,S,m1) - RNS) is ext-real V36() real Element of REAL
0. a is V69(a) 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
((a,S,m1) - RNS) - H1(a) is left_complementable right_complementable complementable Element of the carrier of a
- (0. a) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,m1) - RNS) + (- (0. a)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,m1) - RNS),(- (0. a))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,m1) - RNS) - H1(a)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,m1) - RNS) - H1(a)) is ext-real V36() real Element of REAL
||.H1(a).|| is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() Element of REAL
the normF of a . (0. a) is ext-real V36() real Element of REAL
||.((a,S,m1) - RNS).|| - ||.H1(a).|| is ext-real non negative V36() real Element of REAL
abs (||.((a,S,m1) - RNS).|| - ||.H1(a).||) is ext-real V36() real Element of REAL
(a,(a,S,RNS),m1) is left_complementable right_complementable complementable Element of the carrier of a
||.(a,(a,S,RNS),m1).|| is ext-real non negative V36() real Element of REAL
the normF of a . (a,(a,S,RNS),m1) is ext-real V36() real Element of REAL
||.(a,(a,S,RNS),m1).|| - 0 is ext-real non negative V36() real Element of REAL
abs (||.(a,(a,S,RNS),m1).|| - 0) is ext-real V36() real Element of REAL
||.(a,S,RNS).|| . m1 is ext-real V36() real Element of REAL
(||.(a,S,RNS).|| . m1) - 0 is ext-real V36() real Element of REAL
abs ((||.(a,S,RNS).|| . m1) - 0) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
(a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
S 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:]
(a,RNS,S) 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:]
(a,(a,RNS,S)) is left_complementable right_complementable complementable Element of the carrier of a
(a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS) + (a,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 . ((a,RNS),(a,S)) is left_complementable right_complementable complementable Element of the carrier of a
m1 is ext-real V36() real Element of REAL
m1 / 2 is ext-real V36() real Element of REAL
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k + n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
- (a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - (a,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 . ((a,S,n) - (a,S)) is ext-real V36() real Element of REAL
(a,(a,RNS,S),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) - ((a,RNS) + (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,RNS) + (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) + (- ((a,RNS) + (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,RNS,S),n),(- ((a,RNS) + (a,S)))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,RNS,S),n) - ((a,RNS) + (a,S))).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,(a,RNS,S),n) - ((a,RNS) + (a,S))) is ext-real V36() real Element of REAL
(a,RNS,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(- ((a,RNS) + (a,S))) + ((a,RNS,n) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- ((a,RNS) + (a,S))),((a,RNS,n) + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
||.((- ((a,RNS) + (a,S))) + ((a,RNS,n) + (a,S,n))).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((- ((a,RNS) + (a,S))) + ((a,RNS,n) + (a,S,n))) is ext-real V36() real Element of REAL
- (a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
(- (a,RNS)) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- (a,RNS)),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
((- (a,RNS)) + (- (a,S))) + ((a,RNS,n) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((- (a,RNS)) + (- (a,S))),((a,RNS,n) + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((- (a,RNS)) + (- (a,S))) + ((a,RNS,n) + (a,S,n))).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((- (a,RNS)) + (- (a,S))) + ((a,RNS,n) + (a,S,n))) is ext-real V36() real Element of REAL
(a,RNS,n) + ((- (a,RNS)) + (- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),((- (a,RNS)) + (- (a,S)))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) + ((- (a,RNS)) + (- (a,S)))) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) + ((- (a,RNS)) + (- (a,S)))),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) + ((- (a,RNS)) + (- (a,S)))) + (a,S,n)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) + ((- (a,RNS)) + (- (a,S)))) + (a,S,n)) is ext-real V36() real Element of REAL
(a,RNS,n) - (a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- (a,RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- (a,RNS))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,RNS)) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,RNS)),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - (a,RNS)) + (- (a,S))) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - (a,RNS)) + (- (a,S))),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - (a,RNS)) + (- (a,S))) + (a,S,n)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - (a,RNS)) + (- (a,S))) + (a,S,n)) is ext-real V36() real Element of REAL
((a,RNS,n) - (a,RNS)) + ((a,S,n) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,RNS)),((a,S,n) - (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - (a,RNS)) + ((a,S,n) - (a,S))).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - (a,RNS)) + ((a,S,n) - (a,S))) is ext-real V36() real Element of REAL
||.((a,RNS,n) - (a,RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,n) - (a,RNS)) is ext-real V36() real Element of REAL
||.((a,RNS,n) - (a,RNS)).|| + ||.((a,S,n) - (a,S)).|| is ext-real non negative V36() real Element of REAL
(m1 / 2) + (m1 / 2) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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:]
(a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
S 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:]
(a,RNS,S) 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:]
(a,(a,RNS,S)) is left_complementable right_complementable complementable Element of the carrier of a
(a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
- (a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS) + (- (a,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 . ((a,RNS),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
m1 is ext-real V36() real Element of REAL
m1 / 2 is ext-real V36() real Element of REAL
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k + n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - (a,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 . ((a,S,n) - (a,S)) is ext-real V36() real Element of REAL
(a,(a,RNS,S),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) - ((a,RNS) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,RNS) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,RNS,S),n) + (- ((a,RNS) - (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,RNS,S),n),(- ((a,RNS) - (a,S)))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,RNS,S),n) - ((a,RNS) - (a,S))).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,(a,RNS,S),n) - ((a,RNS) - (a,S))) is ext-real V36() real Element of REAL
(a,RNS,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) - (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
- (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,S,n)) - ((a,RNS) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,S,n)) + (- ((a,RNS) - (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,S,n)),(- ((a,RNS) - (a,S)))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - (a,S,n)) - ((a,RNS) - (a,S))).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - (a,S,n)) - ((a,RNS) - (a,S))) is ext-real V36() real Element of REAL
((a,RNS,n) - (a,S,n)) - (a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
- (a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,S,n)) + (- (a,RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,S,n)),(- (a,RNS))) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - (a,S,n)) - (a,RNS)) + (a,S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - (a,S,n)) - (a,RNS)),(a,S)) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - (a,S,n)) - (a,RNS)) + (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - (a,S,n)) - (a,RNS)) + (a,S)) is ext-real V36() real Element of REAL
(a,RNS) + (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS),(a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) - ((a,RNS) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,RNS) + (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- ((a,RNS) + (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- ((a,RNS) + (a,S,n)))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - ((a,RNS) + (a,S,n))) + (a,S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - ((a,RNS) + (a,S,n))),(a,S)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - ((a,RNS) + (a,S,n))) + (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - ((a,RNS) + (a,S,n))) + (a,S)) is ext-real V36() real Element of REAL
(a,RNS,n) - (a,RNS) is left_complementable right_complementable complementable Element of the carrier of a
(a,RNS,n) + (- (a,RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,RNS,n),(- (a,RNS))) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,RNS)) - (a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,RNS)) + (- (a,S,n)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,RNS)),(- (a,S,n))) is left_complementable right_complementable complementable Element of the carrier of a
(((a,RNS,n) - (a,RNS)) - (a,S,n)) + (a,S) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,RNS,n) - (a,RNS)) - (a,S,n)),(a,S)) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,RNS,n) - (a,RNS)) - (a,S,n)) + (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,RNS,n) - (a,RNS)) - (a,S,n)) + (a,S)) is ext-real V36() real Element of REAL
((a,RNS,n) - (a,RNS)) - ((a,S,n) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,S,n) - (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
((a,RNS,n) - (a,RNS)) + (- ((a,S,n) - (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,RNS,n) - (a,RNS)),(- ((a,S,n) - (a,S)))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,RNS,n) - (a,RNS)) - ((a,S,n) - (a,S))).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,RNS,n) - (a,RNS)) - ((a,S,n) - (a,S))) is ext-real V36() real Element of REAL
||.((a,RNS,n) - (a,RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,RNS,n) - (a,RNS)) is ext-real V36() real Element of REAL
||.((a,RNS,n) - (a,RNS)).|| + ||.((a,S,n) - (a,S)).|| is ext-real non negative V36() real Element of REAL
(m1 / 2) + (m1 / 2) is ext-real V36() real Element of REAL
a is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
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 left_complementable right_complementable complementable Element of the carrier of a
S 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:]
(a,S,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:]
(a,(a,S,RNS)) is left_complementable right_complementable complementable Element of the carrier of a
(a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,S) - RNS is left_complementable right_complementable complementable Element of the carrier of a
- RNS is left_complementable right_complementable complementable Element of the carrier of a
(a,S) + (- 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 . ((a,S),(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
r is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(a,S,n) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
- (a,S) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,S,n) - (a,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 . ((a,S,n) - (a,S)) is ext-real V36() real Element of REAL
0. a is V69(a) 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
(a,S,n) - H1(a) is left_complementable right_complementable complementable Element of the carrier of a
- (0. a) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- (0. a)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (0. a))) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - H1(a)) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - H1(a)) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - H1(a)),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - H1(a)) - (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - H1(a)) - (a,S)) 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 . (RNS,(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) - (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
(a,S,n) + (- (RNS - RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- (RNS - RNS))) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - (RNS - RNS)) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - (RNS - RNS)) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - (RNS - RNS)),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - (RNS - RNS)) - (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - (RNS - RNS)) - (a,S)) is ext-real V36() real Element of REAL
(a,S,n) - RNS is left_complementable right_complementable complementable Element of the carrier of a
(a,S,n) + (- RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,S,n),(- RNS)) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + RNS is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),RNS) is left_complementable right_complementable complementable Element of the carrier of a
(((a,S,n) - RNS) + RNS) - (a,S) is left_complementable right_complementable complementable Element of the carrier of a
(((a,S,n) - RNS) + RNS) + (- (a,S)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((((a,S,n) - RNS) + RNS),(- (a,S))) is left_complementable right_complementable complementable Element of the carrier of a
||.((((a,S,n) - RNS) + RNS) - (a,S)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((((a,S,n) - RNS) + RNS) - (a,S)) is ext-real V36() real Element of REAL
(- (a,S)) + RNS is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((- (a,S)),RNS) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + ((- (a,S)) + RNS) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),((- (a,S)) + RNS)) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - RNS) + ((- (a,S)) + RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - RNS) + ((- (a,S)) + RNS)) is ext-real V36() real Element of REAL
((a,S,n) - RNS) - ((a,S) - RNS) is left_complementable right_complementable complementable Element of the carrier of a
- ((a,S) - RNS) is left_complementable right_complementable complementable Element of the carrier of a
((a,S,n) - RNS) + (- ((a,S) - RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . (((a,S,n) - RNS),(- ((a,S) - RNS))) is left_complementable right_complementable complementable Element of the carrier of a
||.(((a,S,n) - RNS) - ((a,S) - RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . (((a,S,n) - RNS) - ((a,S) - RNS)) is ext-real V36() real Element of REAL
(a,(a,S,RNS),n) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,S,RNS),n) - ((a,S) - RNS) is left_complementable right_complementable complementable Element of the carrier of a
(a,(a,S,RNS),n) + (- ((a,S) - RNS)) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a . ((a,(a,S,RNS),n),(- ((a,S) - RNS))) is left_complementable right_complementable complementable Element of the carrier of a
||.((a,(a,S,RNS),n) - ((a,S) - RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of a . ((a,(a,S,RNS),n) - ((a,S) - RNS)) is ext-real V36() real Element of REAL
a is ext-real V36() real Element of REAL
RNS is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive () ()
the carrier of RNS is non empty set
[:NAT, the carrier of RNS:] is set
bool [:NAT, the carrier of RNS:] is set
S is Relation-like NAT -defined the carrier of RNS -valued Function-like V18( NAT , the carrier of RNS) Element of bool [:NAT, the carrier of RNS:]
(RNS,S,a) is Relation-like NAT -defined the carrier of RNS -valued Function-like V18( NAT , the carrier of RNS) Element of bool [:NAT, the carrier of RNS:]
(RNS,(RNS,S,a)) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S) is left_complementable right_complementable complementable Element of the carrier of RNS
a * (RNS,S) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS is Relation-like [:REAL, the carrier of RNS:] -defined the carrier of RNS -valued Function-like V18([:REAL, the carrier of RNS:], the carrier of RNS) Element of bool [:[:REAL, the carrier of RNS:], the carrier of RNS:]
[:REAL, the carrier of RNS:] is set
[:[:REAL, the carrier of RNS:], the carrier of RNS:] is set
bool [:[:REAL, the carrier of RNS:], the carrier of RNS:] is set
the Mult of RNS . (a,(RNS,S)) is set
r is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) - (RNS,S) is left_complementable right_complementable complementable Element of the carrier of RNS
- (RNS,S) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) + (- (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS is Relation-like [: the carrier of RNS, the carrier of RNS:] -defined the carrier of RNS -valued Function-like V18([: the carrier of RNS, the carrier of RNS:], the carrier of RNS) Element of bool [:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:]
[: the carrier of RNS, the carrier of RNS:] is set
[:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:] is set
bool [:[: the carrier of RNS, the carrier of RNS:], the carrier of RNS:] is set
the addF of RNS . ((RNS,S,n),(- (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,S,n) - (RNS,S)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS is Relation-like the carrier of RNS -defined REAL -valued Function-like V18( the carrier of RNS, REAL ) Element of bool [: the carrier of RNS,REAL:]
[: the carrier of RNS,REAL:] is set
bool [: the carrier of RNS,REAL:] is set
the normF of RNS . ((RNS,S,n) - (RNS,S)) is ext-real V36() real Element of REAL
a * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,(RNS,S,n)) is set
(a * (RNS,S,n)) - (a * (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
- (a * (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- (a * (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- (a * (RNS,S)))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - (a * (RNS,S))).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - (a * (RNS,S))) is ext-real V36() real Element of REAL
0 * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (0,(RNS,S,n)) is set
0. RNS is V69(RNS) left_complementable right_complementable complementable Element of the carrier of RNS
the ZeroF of RNS is left_complementable right_complementable complementable Element of the carrier of RNS
(0 * (RNS,S,n)) - H1(RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
- (0. RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
(0 * (RNS,S,n)) + (- (0. RNS)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((0 * (RNS,S,n)),(- (0. RNS))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((0 * (RNS,S,n)) - H1(RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((0 * (RNS,S,n)) - H1(RNS)) is ext-real V36() real Element of REAL
H1(RNS) - H1(RNS) is left_complementable right_complementable complementable Element of the carrier of RNS
(0. RNS) + (- (0. RNS)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((0. RNS),(- (0. RNS))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.(H1(RNS) - H1(RNS)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . (H1(RNS) - H1(RNS)) is ext-real V36() real Element of REAL
||.H1(RNS).|| is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() Element of REAL
the normF of RNS . (0. RNS) is ext-real V36() real Element of REAL
(RNS,(RNS,S,a),n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) - (a * (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) + (- (a * (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,(RNS,S,a),n),(- (a * (RNS,S)))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,(RNS,S,a),n) - (a * (RNS,S))).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,(RNS,S,a),n) - (a * (RNS,S))) is ext-real V36() real Element of REAL
abs a is ext-real V36() real Element of REAL
0 / (abs a) is ext-real V36() real Element of REAL
r is ext-real V36() real Element of REAL
r / (abs a) is ext-real V36() real Element of REAL
m1 is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() Element of NAT
(RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) - (RNS,S) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,S,n) + (- (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,S,n),(- (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,S,n) - (RNS,S)).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,S,n) - (RNS,S)) is ext-real V36() real Element of REAL
(abs a) * (r / (abs a)) is ext-real V36() real Element of REAL
(abs a) " is ext-real V36() real Element of REAL
((abs a) ") * r is ext-real V36() real Element of REAL
(abs a) * (((abs a) ") * r) is ext-real V36() real Element of REAL
(abs a) * ((abs a) ") is ext-real V36() real Element of REAL
((abs a) * ((abs a) ")) * r is ext-real V36() real Element of REAL
1 * r is ext-real V36() real Element of REAL
a * (RNS,S,n) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,(RNS,S,n)) is set
(a * (RNS,S,n)) - (a * (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
(a * (RNS,S,n)) + (- (a * (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((a * (RNS,S,n)),(- (a * (RNS,S)))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((a * (RNS,S,n)) - (a * (RNS,S))).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((a * (RNS,S,n)) - (a * (RNS,S))) is ext-real V36() real Element of REAL
a * ((RNS,S,n) - (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
the Mult of RNS . (a,((RNS,S,n) - (RNS,S))) is set
||.(a * ((RNS,S,n) - (RNS,S))).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . (a * ((RNS,S,n) - (RNS,S))) is ext-real V36() real Element of REAL
(abs a) * ||.((RNS,S,n) - (RNS,S)).|| is ext-real V36() real Element of REAL
(RNS,(RNS,S,a),n) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) - (a * (RNS,S)) is left_complementable right_complementable complementable Element of the carrier of RNS
(RNS,(RNS,S,a),n) + (- (a * (RNS,S))) is left_complementable right_complementable complementable Element of the carrier of RNS
the addF of RNS . ((RNS,(RNS,S,a),n),(- (a * (RNS,S)))) is left_complementable right_complementable complementable Element of the carrier of RNS
||.((RNS,(RNS,S,a),n) - (a * (RNS,S))).|| is ext-real non negative V36() real Element of REAL
the normF of RNS . ((RNS,(RNS,S,a),n) - (a * (RNS,S))) is ext-real V36() real Element of REAL