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