:: RLVECT_1 semantic presentation

REAL is non empty V38() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V38() cardinal limit_cardinal Element of bool REAL
bool REAL is V38() set
omega is non empty epsilon-transitive epsilon-connected ordinal V38() cardinal limit_cardinal set
bool omega is V38() set
bool NAT is V38() set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
{{},1} is non empty set
[:1,1:] is Relation-like set
bool [:1,1:] is set
[:[:1,1:],1:] is Relation-like set
bool [:[:1,1:],1:] is set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial V38() 1 -element Element of bool NAT
{1} is non empty trivial 1 -element set
Seg 2 is non empty V38() 2 -element Element of bool NAT
{1,2} is non empty set
{{}} is functional non empty trivial 1 -element set
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 Relation-like set
[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like 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 Relation-like V38() set
[:[:REAL, the non empty set :], the non empty set :] is Relation-like V38() set
bool [:[:REAL, the non empty set :], the non empty set :] is V38() 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 , 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 :]) 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 :]) is set
V is non empty 1-sorted
the carrier of V is non empty set
v is Element of the carrier of V
V is non empty ()
the carrier of V is non empty set
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
w is ext-real V36() real set
v is Element of the carrier of V
the of V . (w,v) is set
w is ext-real V36() real Element of REAL
the of V . (w,v) is Element of the carrier of V
V is non empty addMagma
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is Element of the carrier of V
V is non empty set
[:V,V:] is Relation-like set
[:[:V,V:],V:] is Relation-like set
bool [:[:V,V:],V:] is set
[:REAL,V:] is Relation-like V38() set
[:[:REAL,V:],V:] is Relation-like V38() set
bool [:[:REAL,V:],V:] is V38() set
v is Element of V
w is Relation-like [:V,V:] -defined V -valued Function-like V18([:V,V:],V) Element of bool [:[:V,V:],V:]
w is Relation-like [:REAL,V:] -defined V -valued Function-like V18([:REAL,V:],V) Element of bool [:[:REAL,V:],V:]
(V,v,w,w) is () ()
op0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of 1
op2 is Relation-like [:1,1:] -defined 1 -valued Function-like V18([:1,1:],1) Element of bool [:[:1,1:],1:]
pr2 (REAL,1) is Relation-like [:REAL,1:] -defined 1 -valued Function-like V18([:REAL,1:],1) Element of bool [:[:REAL,1:],1:]
[:REAL,1:] is Relation-like V38() set
[:[:REAL,1:],1:] is Relation-like V38() set
bool [:[:REAL,1:],1:] is V38() set
(1,op0,op2,(pr2 (REAL,1))) is non empty () ()
() is () ()
the carrier of () is set
Trivial-addMagma is non empty trivial V56() 1 -element strict left_add-cancelable right_add-cancelable add-cancelable addMagma
addMagma(# 1,op2 #) is non empty strict addMagma
V is non empty trivial V56() 1 -element strict left_add-cancelable right_add-cancelable add-cancelable addMagma
the carrier of V is non empty trivial V38() 1 -element set
v is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
v + w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
w + v is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V . (w,v) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
v + w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
(v + w) + w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V . ((v + w),w) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
w + w is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V . (w,w) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
v + (w + w) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
the addF of V . (v,(w + w)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of V
Trivial-addLoopStr is non empty trivial V56() 1 -element left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable addLoopStr
addLoopStr(# 1,op2,op0 #) is non empty strict addLoopStr
V is non empty trivial V56() 1 -element left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable addLoopStr
the carrier of V is non empty trivial V38() 1 -element set
v is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
v + w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
w + v is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (w,v) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
v + w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
(v + w) + w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((v + w),w) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
w + w is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (w,w) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
v + (w + w) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (v,(w + w)) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
0. V is V57(V) left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
v + (0. V) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(0. V)) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of V
V is non empty trivial V56() 1 -element () ()
the carrier of V is non empty trivial V38() 1 -element set
v is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is Element of the carrier of V
w + v is Element of the carrier of V
the addF of V . (w,v) is Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is Element of the carrier of V
w is Element of the carrier of V
(v + w) + w is Element of the carrier of V
the addF of V . ((v + w),w) is Element of the carrier of V
w + w is Element of the carrier of V
the addF of V . (w,w) is Element of the carrier of V
v + (w + w) is Element of the carrier of V
the addF of V . (v,(w + w)) is Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is Element of the carrier of V
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
v + (0. V) is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(0. V)) is Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
v is Element of the carrier of V
v + v is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,v) is Element of the carrier of V
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the carrier of V is non empty trivial V38() 1 -element set
w is Element of the carrier of V
v is ext-real V36() real set
w is ext-real V36() real set
v + w is ext-real V36() real set
(V,w,(v + w)) is Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . ((v + w),w) is set
(V,w,v) is Element of the carrier of V
the of V . (v,w) is set
(V,w,w) is Element of the carrier of V
the of V . (w,w) is set
(V,w,v) + (V,w,w) is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . ((V,w,v),(V,w,w)) is Element of the carrier of V
w is Element of the carrier of V
w is Element of the carrier of V
w + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (w,w) is Element of the carrier of V
v is ext-real V36() real set
(V,(w + w),v) is Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . (v,(w + w)) is set
(V,w,v) is Element of the carrier of V
the of V . (v,w) is set
(V,w,v) is Element of the carrier of V
the of V . (v,w) is set
(V,w,v) + (V,w,v) is Element of the carrier of V
the addF of V . ((V,w,v),(V,w,v)) is Element of the carrier of V
w is Element of the carrier of V
v is ext-real V36() real set
w is ext-real V36() real set
v * w is ext-real V36() real set
(V,w,(v * w)) is Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . ((v * w),w) is set
(V,w,w) is Element of the carrier of V
the of V . (w,w) is set
(V,(V,w,w),v) is Element of the carrier of V
the of V . (v,(V,w,w)) is set
v is Element of the carrier of V
(V,v,1) is Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . (1,v) is set
V is () addMagma
the carrier of V is set
w is Element of the carrier of V
v is Element of the carrier of V
w + v is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (w,v) is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V . (v,w) is Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w + w is right_complementable Element of the carrier of V
the addF of V . (w,w) is right_complementable Element of the carrier of V
v + (w + w) is right_complementable Element of the carrier of V
the addF of V . (v,(w + w)) is right_complementable Element of the carrier of V
w + (v + (w + w)) is right_complementable Element of the carrier of V
the addF of V . (w,(v + (w + w))) is right_complementable Element of the carrier of V
(v + w) + w is right_complementable Element of the carrier of V
the addF of V . ((v + w),w) is right_complementable Element of the carrier of V
w + ((v + w) + w) is right_complementable Element of the carrier of V
the addF of V . (w,((v + w) + w)) is right_complementable Element of the carrier of V
w + (v + w) is right_complementable Element of the carrier of V
the addF of V . (w,(v + w)) is right_complementable Element of the carrier of V
(w + (v + w)) + w is right_complementable Element of the carrier of V
the addF of V . ((w + (v + w)),w) is right_complementable Element of the carrier of V
V is right_complementable () () addLoopStr
the carrier of V is set
v is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
v + v is right_complementable Element of the carrier of V
the addF of V . (v,v) is right_complementable Element of the carrier of V
w + (0. V) is right_complementable Element of the carrier of V
the addF of V . (w,(0. V)) is right_complementable Element of the carrier of V
(w + v) + w is right_complementable Element of the carrier of V
the addF of V . ((w + v),w) is right_complementable Element of the carrier of V
v + (0. V) is right_complementable Element of the carrier of V
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
v + (0. V) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
(0. V) + v is right_complementable Element of the carrier of V
the addF of V . ((0. V),v) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V . (v,w) is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
v is Element of the carrier of V
- v is Element of the carrier of V
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V . (v,w) is Element of the carrier of V
w + v is Element of the carrier of V
the addF of V . (w,v) is Element of the carrier of V
(w + v) + w is Element of the carrier of V
the addF of V . ((w + v),w) is Element of the carrier of V
w + (0. V) is Element of the carrier of V
the addF of V . (w,(0. V)) is Element of the carrier of V
(0. V) + w is Element of the carrier of V
the addF of V . ((0. V),w) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
(v + (- v)) + v is Element of the carrier of V
the addF of V . ((v + (- v)),v) is Element of the carrier of V
(- v) + v is Element of the carrier of V
the addF of V . ((- v),v) is Element of the carrier of V
v + ((- v) + v) is Element of the carrier of V
the addF of V . (v,((- v) + v)) is Element of the carrier of V
v + (0. V) is Element of the carrier of V
the addF of V . (v,(0. V)) is Element of the carrier of V
(0. V) + v is Element of the carrier of V
the addF of V . ((0. V),v) is Element of the carrier of V
(0. V) + w is Element of the carrier of V
the addF of V . ((0. V),w) is Element of the carrier of V
((- v) + v) + w is Element of the carrier of V
the addF of V . (((- v) + v),w) is Element of the carrier of V
(- v) + (0. V) is Element of the carrier of V
the addF of V . ((- v),(0. V)) is Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(- v) + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . ((- v),w) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V . (v,w) is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
(v + (- v)) + w is right_complementable Element of the carrier of V
the addF of V . ((v + (- v)),w) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(0. V) + w is right_complementable Element of the carrier of V
the addF of V . ((0. V),w) is right_complementable Element of the carrier of V
V is addLoopStr
the carrier of V is set
v is Element of the carrier of V
w is Element of the carrier of V
v - w is Element of the carrier of V
- w is Element of the carrier of V
v + (- w) is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- w)) is Element of the carrier of V
w is Element of the carrier of V
v is Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
(- v) + v is right_complementable Element of the carrier of V
the addF of V . ((- v),v) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
v + v is right_complementable Element of the carrier of V
the addF of V . (v,v) is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
v + v is right_complementable Element of the carrier of V
the addF of V . (v,v) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
w + (0. V) is right_complementable Element of the carrier of V
the addF of V . (w,(0. V)) is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
w + (v + (- v)) is right_complementable Element of the carrier of V
the addF of V . (w,(v + (- v))) is right_complementable Element of the carrier of V
(w + v) + (- v) is right_complementable Element of the carrier of V
the addF of V . ((w + v),(- v)) is right_complementable Element of the carrier of V
v + (v + (- v)) is right_complementable Element of the carrier of V
the addF of V . (v,(v + (- v))) is right_complementable Element of the carrier of V
v + (0. V) is right_complementable Element of the carrier of V
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
(0. V) + w is right_complementable Element of the carrier of V
the addF of V . ((0. V),w) is right_complementable Element of the carrier of V
(- v) + v is right_complementable Element of the carrier of V
the addF of V . ((- v),v) is right_complementable Element of the carrier of V
((- v) + v) + w is right_complementable Element of the carrier of V
the addF of V . (((- v) + v),w) is right_complementable Element of the carrier of V
(- v) + (v + w) is right_complementable Element of the carrier of V
the addF of V . ((- v),(v + w)) is right_complementable Element of the carrier of V
((- v) + v) + v is right_complementable Element of the carrier of V
the addF of V . (((- v) + v),v) is right_complementable Element of the carrier of V
(0. V) + v is right_complementable Element of the carrier of V
the addF of V . ((0. V),v) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
w + v is right_complementable Element of the carrier of V
the addF of V . (w,v) is right_complementable Element of the carrier of V
v + (0. V) is right_complementable Element of the carrier of V
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
(0. V) + v is right_complementable Element of the carrier of V
the addF of V . ((0. V),v) is right_complementable Element of the carrier of V
V is ext-real V36() real set
v is non empty right_complementable () () () () () () () ()
the carrier of v is non empty set
0. v is V57(v) right_complementable Element of the carrier of v
the ZeroF of v is right_complementable Element of the carrier of v
w is right_complementable Element of the carrier of v
(v,w,V) is right_complementable Element of the carrier of v
the of v is Relation-like [:REAL, the carrier of v:] -defined the carrier of v -valued Function-like V18([:REAL, the carrier of v:], the carrier of v) Element of bool [:[:REAL, the carrier of v:], the carrier of v:]
[:REAL, the carrier of v:] is Relation-like V38() set
[:[:REAL, the carrier of v:], the carrier of v:] is Relation-like V38() set
bool [:[:REAL, the carrier of v:], the carrier of v:] is V38() set
the of v . (V,w) is set
(v,w,0) is right_complementable Element of the carrier of v
the of v . (0,w) is set
(v,w,(v,w,0)) is right_complementable Element of the carrier of v
the addF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V18([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is Relation-like set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is Relation-like set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is set
the addF of v . (w,(v,w,0)) is right_complementable Element of the carrier of v
(v,w,1) is right_complementable Element of the carrier of v
the of v . (1,w) is set
(v,(v,w,1),(v,w,0)) is right_complementable Element of the carrier of v
the addF of v . ((v,w,1),(v,w,0)) is right_complementable Element of the carrier of v
1 + 0 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(v,w,(1 + 0)) is right_complementable Element of the carrier of v
the of v . ((1 + 0),w) is set
(v,w,(0. v)) is right_complementable Element of the carrier of v
the addF of v . (w,(0. v)) is right_complementable Element of the carrier of v
(v,(0. v),V) is right_complementable Element of the carrier of v
the of v . (V,(0. v)) is set
(v,(v,(0. v),V),(v,(0. v),V)) is right_complementable Element of the carrier of v
the addF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V18([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is Relation-like set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is Relation-like set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is set
the addF of v . ((v,(0. v),V),(v,(0. v),V)) is right_complementable Element of the carrier of v
(v,(0. v),(0. v)) is right_complementable Element of the carrier of v
the addF of v . ((0. v),(0. v)) is right_complementable Element of the carrier of v
(v,(v,(0. v),(0. v)),V) is right_complementable Element of the carrier of v
the of v . (V,(v,(0. v),(0. v))) is set
(v,(v,(0. v),V),(0. v)) is right_complementable Element of the carrier of v
the addF of v . ((v,(0. v),V),(0. v)) is right_complementable Element of the carrier of v
V is ext-real V36() real set
v is non empty right_complementable () () () () () () () ()
the carrier of v is non empty set
0. v is V57(v) right_complementable Element of the carrier of v
the ZeroF of v is right_complementable Element of the carrier of v
w is right_complementable Element of the carrier of v
(v,w,V) is right_complementable Element of the carrier of v
the of v is Relation-like [:REAL, the carrier of v:] -defined the carrier of v -valued Function-like V18([:REAL, the carrier of v:], the carrier of v) Element of bool [:[:REAL, the carrier of v:], the carrier of v:]
[:REAL, the carrier of v:] is Relation-like V38() set
[:[:REAL, the carrier of v:], the carrier of v:] is Relation-like V38() set
bool [:[:REAL, the carrier of v:], the carrier of v:] is V38() set
the of v . (V,w) is set
(v,w,1) is right_complementable Element of the carrier of v
the of v . (1,w) is set
V " is ext-real V36() real set
(V ") * V is ext-real V36() real set
(v,w,((V ") * V)) is right_complementable Element of the carrier of v
the of v . (((V ") * V),w) is set
(v,(0. v),(V ")) is right_complementable Element of the carrier of v
the of v . ((V "),(0. v)) is set
V is non empty right_complementable () () addLoopStr
0. V is V57(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V
- (0. V) is right_complementable Element of the carrier of V
(0. V) + (- (0. V)) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . ((0. V),(- (0. V))) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
v - (0. V) is right_complementable Element of the carrier of V
- (0. V) is right_complementable Element of the carrier of V
v + (- (0. V)) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- (0. V))) is right_complementable Element of the carrier of V
v + (0. V) is right_complementable Element of the carrier of V
the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
(0. V) - v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(0. V) + (- v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . ((0. V),(- v)) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
v - v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
- 1 is ext-real non positive V36() real Element of REAL
V is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(V,v,(- 1)) is right_complementable Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . ((- 1),v) is set
(V,v,(V,v,(- 1))) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(V,v,(- 1))) is right_complementable Element of the carrier of V
(V,v,1) is right_complementable Element of the carrier of V
the of V . (1,v) is set
(V,(V,v,1),(V,v,(- 1))) is right_complementable Element of the carrier of V
the addF of V . ((V,v,1),(V,v,(- 1))) is right_complementable Element of the carrier of V
1 + (- 1) is ext-real V36() real Element of REAL
(V,v,(1 + (- 1))) is right_complementable Element of the carrier of V
the of V . ((1 + (- 1)),v) is set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(V,(- v),(V,v,(V,v,(- 1)))) is right_complementable Element of the carrier of V
the addF of V . ((- v),(V,v,(V,v,(- 1)))) is right_complementable Element of the carrier of V
(V,(- v),v) is right_complementable Element of the carrier of V
the addF of V . ((- v),v) is right_complementable Element of the carrier of V
(V,(V,(- v),v),(V,v,(- 1))) is right_complementable Element of the carrier of V
the addF of V . ((V,(- v),v),(V,v,(- 1))) is right_complementable Element of the carrier of V
(V,(0. V),(V,v,(- 1))) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(V,v,(- 1))) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
- (- v) is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
- (- w) is right_complementable Element of the carrier of V
V is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(V,v,v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,v) is right_complementable Element of the carrier of V
(V,v,1) is right_complementable Element of the carrier of V
the of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is Relation-like V38() set
[:[:REAL, the carrier of V:], the carrier of V:] is Relation-like V38() set
bool [:[:REAL, the carrier of V:], the carrier of V:] is V38() set
the of V . (1,v) is set
(V,(V,v,1),v) is right_complementable Element of the carrier of V
the addF of V . ((V,v,1),v) is right_complementable Element of the carrier of V
(V,(V,v,1),(V,v,1)) is right_complementable Element of the carrier of V
the addF of V . ((V,v,1),(V,v,1)) is right_complementable Element of the carrier of V
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,v,(1 + 1)) is right_complementable Element of the carrier of V
the of V . ((1 + 1),v) is set
(V,v,2) is right_complementable Element of the carrier of V
the of V . (2,v) is set
V is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
(V,v,v) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,v) is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
v + (- w) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- w)) is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
w is right_complementable Element of the carrier of V
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (w,w) is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
w - (- w) is right_complementable Element of the carrier of V
- (- w) is right_complementable Element of the carrier of V
w + (- (- w)) is right_complementable Element of the carrier of V
the addF of V . (w,(- (- w))) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
v + (- w) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,(- w)) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
v + (- w) is right_complementable Element of the carrier of V
the addF of V . (v,(- w)) is right_complementable Element of the carrier of V
V is ext-real V36() real set
- V is ext-real V36() real set
v is non empty right_complementable () () () () () () () ()
the carrier of v is non empty set
w is right_complementable Element of the carrier of v
- w is right_complementable Element of the carrier of v
(v,(- w),V) is right_complementable Element of the carrier of v
the of v is Relation-like [:REAL, the carrier of v:] -defined the carrier of v -valued Function-like V18([:REAL, the carrier of v:], the carrier of v) Element of bool [:[:REAL, the carrier of v:], the carrier of v:]
[:REAL, the carrier of v:] is Relation-like V38() set
[:[:REAL, the carrier of v:], the carrier of v:] is Relation-like V38() set
bool [:[:REAL, the carrier of v:], the carrier of v:] is V38() set
the of v . (V,(- w)) is set
(v,w,(- V)) is right_complementable Element of the carrier of v
the of v . ((- V),w) is set
(v,w,(- 1)) is right_complementable Element of the carrier of v
the of v . ((- 1),w) is set
(v,(v,w,(- 1)),V) is right_complementable Element of the carrier of v
the of v . (V,(v,w,(- 1))) is set
V * (- 1) is ext-real V36() real Element of REAL
(v,w,(V * (- 1))) is right_complementable Element of the carrier of v
the of v . ((V * (- 1)),w) is set
V is ext-real V36() real set
v is non empty right_complementable () () () () () () () ()
the carrier of v is non empty set
w is right_complementable Element of the carrier of v
- w is right_complementable Element of the carrier of v
(v,(- w),V) is right_complementable Element of the carrier of v
the of v is Relation-like [:REAL, the carrier of v:] -defined the carrier of v -valued Function-like V18([:REAL, the carrier of v:], the carrier of v) Element of bool [:[:REAL, the carrier of v:], the carrier of v:]
[:REAL, the carrier of v:] is Relation-like V38() set
[:[:REAL, the carrier of v:], the carrier of v:] is Relation-like V38() set
bool [:[:REAL, the carrier of v:], the carrier of v:] is V38() set
the of v . (V,(- w)) is set
(v,w,V) is right_complementable Element of the carrier of v
the of v . (V,w) is set
- (v,w,V) is right_complementable Element of the carrier of v
1 * V is ext-real V36() real Element of REAL
- (1 * V) is ext-real V36() real Element of REAL
(v,w,(- (1 * V))) is right_complementable Element of the carrier of v
the of v . ((- (1 * V)),w) is set
(- 1) * V is ext-real V36() real Element of REAL
(v,w,((- 1) * V)) is right_complementable Element of the carrier of v
the of v . (((- 1) * V),w) is set
(v,(v,w,V),(- 1)) is right_complementable Element of the carrier of v
the of v . ((- 1),(v,w,V)) is set
V is ext-real V36() real set
- V is ext-real V36() real set
v is non empty right_complementable () () () () () () () ()
the carrier of v is non empty set
w is right_complementable Element of the carrier of v
- w is right_complementable Element of the carrier of v
(v,(- w),(- V)) is right_complementable Element of the carrier of v
the of v is Relation-like [:REAL, the carrier of v:] -defined the carrier of v -valued Function-like V18([:REAL, the carrier of v:], the carrier of v) Element of bool [:[:REAL, the carrier of v:], the carrier of v:]
[:REAL, the carrier of v:] is Relation-like V38() set
[:[:REAL, the carrier of v:], the carrier of v:] is Relation-like V38() set
bool [:[:REAL, the carrier of v:], the carrier of v:] is V38() set
the of v . ((- V),(- w)) is set
(v,w,V) is right_complementable Element of the carrier of v
the of v . (V,w) is set
- (- V) is ext-real V36() real set
(v,w,(- (- V))) is right_complementable Element of the carrier of v
the of v . ((- (- V)),w) is set
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
- (v + w) is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(- w) + (- v) is right_complementable Element of the carrier of V
the addF of V . ((- w),(- v)) is right_complementable Element of the carrier of V
(v + w) + ((- w) + (- v)) is right_complementable Element of the carrier of V
the addF of V . ((v + w),((- w) + (- v))) is right_complementable Element of the carrier of V
w + ((- w) + (- v)) is right_complementable Element of the carrier of V
the addF of V . (w,((- w) + (- v))) is right_complementable Element of the carrier of V
v + (w + ((- w) + (- v))) is right_complementable Element of the carrier of V
the addF of V . (v,(w + ((- w) + (- v)))) is right_complementable Element of the carrier of V
w + (- w) is right_complementable Element of the carrier of V
the addF of V . (w,(- w)) is right_complementable Element of the carrier of V
(w + (- w)) + (- v) is right_complementable Element of the carrier of V
the addF of V . ((w + (- w)),(- v)) is right_complementable Element of the carrier of V
v + ((w + (- w)) + (- v)) is right_complementable Element of the carrier of V
the addF of V . (v,((w + (- w)) + (- v))) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(0. V) + (- v) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(- v)) is right_complementable Element of the carrier of V
v + ((0. V) + (- v)) is right_complementable Element of the carrier of V
the addF of V . (v,((0. V) + (- v))) is right_complementable Element of the carrier of V
v + (- v) is right_complementable Element of the carrier of V
the addF of V . (v,(- v)) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (w,w) is right_complementable Element of the carrier of V
v - (w + w) is right_complementable Element of the carrier of V
- (w + w) is right_complementable Element of the carrier of V
v + (- (w + w)) is right_complementable Element of the carrier of V
the addF of V . (v,(- (w + w))) is right_complementable Element of the carrier of V
v - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
v + (- w) is right_complementable Element of the carrier of V
the addF of V . (v,(- w)) is right_complementable Element of the carrier of V
(v - w) - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
(v - w) + (- w) is right_complementable Element of the carrier of V
the addF of V . ((v - w),(- w)) is right_complementable Element of the carrier of V
(- w) + (- w) is right_complementable Element of the carrier of V
the addF of V . ((- w),(- w)) is right_complementable Element of the carrier of V
v + ((- w) + (- w)) is right_complementable Element of the carrier of V
the addF of V . (v,((- w) + (- w))) is right_complementable Element of the carrier of V
V is non empty () addLoopStr
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
v + w is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is Element of the carrier of V
w is Element of the carrier of V
(v + w) - w is Element of the carrier of V
- w is Element of the carrier of V
(v + w) + (- w) is Element of the carrier of V
the addF of V . ((v + w),(- w)) is Element of the carrier of V
w - w is Element of the carrier of V
w + (- w) is Element of the carrier of V
the addF of V . (w,(- w)) is Element of the carrier of V
v + (w - w) is Element of the carrier of V
the addF of V . (v,(w - w)) is Element of the carrier of V
V is non empty right_complementable () () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
w - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
w + (- w) is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (w,(- w)) is right_complementable Element of the carrier of V
v - (w - w) is right_complementable Element of the carrier of V
- (w - w) is right_complementable Element of the carrier of V
v + (- (w - w)) is right_complementable Element of the carrier of V
the addF of V . (v,(- (w - w))) is right_complementable Element of the carrier of V
v - w is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
v + (- w) is right_complementable Element of the carrier of V
the addF of V . (v,(- w)) is right_complementable Element of the carrier of V
(V,(v - w),w) is right_complementable Element of the carrier of V
the addF of V . ((v - w),w) is right_complementable Element of the carrier of V
(V,w,(- w)) is right_complementable Element of the carrier of V
v - (V,w,(- w)) is right_complementable Element of the carrier of V
- (V,w,(- w)) is right_complementable Element of the carrier of V
v + (- (V,w,(- w))) is right_complementable Element of the carrier of V
the addF of V . (v,(- (V,w,(- w)))) is right_complementable Element of the carrier of V
(v - w) - (- w) is right_complementable Element of the carrier of V
- (- w) is right_complementable Element of the carrier of V
(v - w) + (- (- w)) is right_complementable Element of the carrier of V
the addF of V . ((v - w),(- (- w))) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is set
the addF of V . (v,w) is right_complementable Element of the carrier of V
- (v + w) is right_complementable Element of the carrier of V
- w is right_complementable Element of the carrier of V
(- w) - v is right_complementable Element of the carrier of V
- v is right_complementable Element of the carrier of V
(- w) + (- v) is right_complementable Element of the carrier of V
the addF of V . ((- w),(- v)) is right_complementable Element of the carrier of V
0. V is V57(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(0. V) - (v + w) is right_complementable Element of the carrier of V
(0. V) + (- (v + w)) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(- (v + w))) is right_complementable Element of the carrier of V
(0. V) - w is right_complementable Element of the carrier of V
(0. V) + (- w) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(- w)) is right_complementable Element of the carrier of V
((0. V) - w) - v is right_complementable Element of the carrier of V
((0. V) - w) + (- v) is right_complementable Element of the carrier of V
the addF of V . (((0. V) - w),(- v)) is right_complementable Element of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
v + w is right_complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like set