:: 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
[:[: 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 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
(- 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) - 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,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,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
- 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
- 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
- (- 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 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
(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
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),V) is right_complementable Element of the carrier of v
the of v . (V,(w - 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) - (v,w,V) is right_complementable Element of the carrier of v
- (v,w,V) is right_complementable Element of the carrier of v
(v,w,V) + (- (v,w,V)) is right_complementable Element of the carrier of v
the addF of v . ((v,w,V),(- (v,w,V))) is right_complementable Element of the carrier of v
(v,(- w),V) is right_complementable Element of the carrier of v
the of v . (V,(- w)) is set
(v,(v,w,V),(v,(- w),V)) is right_complementable Element of the carrier of v
the addF of v . ((v,w,V),(v,(- w),V)) is right_complementable Element of the carrier of v
V is ext-real V36() real set
v is ext-real V36() real set
V - v is ext-real V36() real set
w is non empty right_complementable () () () () () () () ()
the carrier of w is non empty set
w is right_complementable Element of the carrier of w
(w,w,(V - v)) is right_complementable Element of the carrier of w
the of w is Relation-like [:REAL, the carrier of w:] -defined the carrier of w -valued Function-like V18([:REAL, the carrier of w:], the carrier of w) Element of bool [:[:REAL, the carrier of w:], the carrier of w:]
[:REAL, the carrier of w:] is Relation-like V38() set
[:[:REAL, the carrier of w:], the carrier of w:] is Relation-like V38() set
bool [:[:REAL, the carrier of w:], the carrier of w:] is V38() set
the of w . ((V - v),w) is set
(w,w,V) is right_complementable Element of the carrier of w
the of w . (V,w) is set
(w,w,v) is right_complementable Element of the carrier of w
the of w . (v,w) is set
(w,w,V) - (w,w,v) is right_complementable Element of the carrier of w
- (w,w,v) is right_complementable Element of the carrier of w
(w,w,V) + (- (w,w,v)) is right_complementable Element of the carrier of w
the addF of w is Relation-like [: the carrier of w, the carrier of w:] -defined the carrier of w -valued Function-like V18([: the carrier of w, the carrier of w:], the carrier of w) Element of bool [:[: the carrier of w, the carrier of w:], the carrier of w:]
[: the carrier of w, the carrier of w:] is Relation-like set
[:[: the carrier of w, the carrier of w:], the carrier of w:] is Relation-like set
bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is set
the addF of w . ((w,w,V),(- (w,w,v))) is right_complementable Element of the carrier of w
- v is ext-real V36() real set
V + (- v) is ext-real V36() real set
(w,w,(V + (- v))) is right_complementable Element of the carrier of w
the of w . ((V + (- v)),w) is set
(w,w,(- v)) is right_complementable Element of the carrier of w
the of w . ((- v),w) is set
(w,(w,w,V),(w,w,(- v))) is right_complementable Element of the carrier of w
the addF of w . ((w,w,V),(w,w,(- v))) is right_complementable Element of the carrier of w
- w is right_complementable Element of the carrier of w
(w,(- w),v) is right_complementable Element of the carrier of w
the of w . (v,(- w)) is set
(w,(w,w,V),(w,(- w),v)) is right_complementable Element of the carrier of w
the addF of w . ((w,w,V),(w,(- w),v)) is right_complementable Element of the carrier of w
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
(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
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 . (V,w) 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,w,V) - (v,w,V) is right_complementable Element of the carrier of v
- (v,w,V) is right_complementable Element of the carrier of v
(v,w,V) + (- (v,w,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,w,V),(- (v,w,V))) 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,(w - w),V) is right_complementable Element of the carrier of v
the of v . (V,(w - w)) is set
V is ext-real V36() real set
v is ext-real V36() real set
w is non empty right_complementable () () () () () () () ()
the carrier of w is non empty set
0. w is V57(w) right_complementable Element of the carrier of w
the ZeroF of w is right_complementable Element of the carrier of w
w is right_complementable Element of the carrier of w
(w,w,V) is right_complementable Element of the carrier of w
the of w is Relation-like [:REAL, the carrier of w:] -defined the carrier of w -valued Function-like V18([:REAL, the carrier of w:], the carrier of w) Element of bool [:[:REAL, the carrier of w:], the carrier of w:]
[:REAL, the carrier of w:] is Relation-like V38() set
[:[:REAL, the carrier of w:], the carrier of w:] is Relation-like V38() set
bool [:[:REAL, the carrier of w:], the carrier of w:] is V38() set
the of w . (V,w) is set
(w,w,v) is right_complementable Element of the carrier of w
the of w . (v,w) is set
(w,w,V) - (w,w,v) is right_complementable Element of the carrier of w
- (w,w,v) is right_complementable Element of the carrier of w
(w,w,V) + (- (w,w,v)) is right_complementable Element of the carrier of w
the addF of w is Relation-like [: the carrier of w, the carrier of w:] -defined the carrier of w -valued Function-like V18([: the carrier of w, the carrier of w:], the carrier of w) Element of bool [:[: the carrier of w, the carrier of w:], the carrier of w:]
[: the carrier of w, the carrier of w:] is Relation-like set
[:[: the carrier of w, the carrier of w:], the carrier of w:] is Relation-like set
bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is set
the addF of w . ((w,w,V),(- (w,w,v))) is right_complementable Element of the carrier of w
V - v is ext-real V36() real set
(w,w,(V - v)) is right_complementable Element of the carrier of w
the of w . ((V - v),w) is set
- v is ext-real V36() real set
(- v) + V is ext-real V36() real set
V is non empty addLoopStr
the carrier of V is non empty set
[:NAT, the carrier of V:] is Relation-like V38() set
bool [:NAT, the carrier of V:] is V38() set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like set
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like set
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
rng w is set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Seg w is V38() w -element Element of bool NAT
v | (Seg w) is Relation-like NAT -defined Seg w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
dom w is Element of bool NAT
Seg (w + 1) is non empty V38() w + 1 -element Element of bool NAT
w . (w + 1) is set
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Element of the carrier of V
n is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
n . (len I) is Element of the carrier of V
n . 0 is Element of the carrier of V
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
n . m2 is set
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x is Element of the carrier of V
(n . (len I)) + x 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 . ((n . (len I)),x) is Element of the carrier of V
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 is Element of the carrier of V
n . m2 is Element of the carrier of V
m1 is Element of the carrier of V
(n . (len I)) + m1 is Element of the carrier of V
the addF of V . ((n . (len I)),m1) is Element of the carrier of V
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 is Element of the carrier of V
m1 is Element of the carrier of V
(n . (len I)) + m1 is Element of the carrier of V
the addF of V . ((n . (len I)),m1) is Element of the carrier of V
q2 is Element of the carrier of V
p is Element of the carrier of V
m2 is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
m2 . (w + 1) is Element of the carrier of V
m2 is Element of the carrier of V
q2 is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
q2 . (len w) is Element of the carrier of V
q2 . 0 is Element of the carrier of V
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w . (p + 1) is set
q2 . (p + 1) is Element of the carrier of V
q2 . p is Element of the carrier of V
m1 is Element of the carrier of V
(q2 . p) + m1 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 . ((q2 . p),m1) is Element of the carrier of V
n . p is Element of the carrier of V
(n . p) + m1 is Element of the carrier of V
the addF of V . ((n . p),m1) is Element of the carrier of V
1 + p is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (p + 1) is set
n . (p + 1) is Element of the carrier of V
m2 . p is Element of the carrier of V
(m2 . p) + m1 is Element of the carrier of V
the addF of V . ((m2 . p),m1) is Element of the carrier of V
NAT --> (0. V) is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) T-Sequence-like Element of bool [:NAT, the carrier of V:]
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like set
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
w . (len w) is Element of the carrier of V
v is Element of the carrier of V
I is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
I . (len w) is Element of the carrier of V
I . 0 is Element of the carrier of V
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w . (x + 1) is set
I . (x + 1) is Element of the carrier of V
I . x is Element of the carrier of V
v is Element of the carrier of V
(I . x) + 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 . ((I . x),v) is Element of the carrier of V
w is Element of the carrier of V
w is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
v . (len v) is Element of the carrier of V
v . 0 is Element of the carrier of V
I is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
I . (len v) is Element of the carrier of V
I . 0 is Element of the carrier of V
rng v is set
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . x is Element of the carrier of V
I . x is Element of the carrier of V
x + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
dom v is Element of bool NAT
Seg (len v) is V38() len v -element Element of bool NAT
v . (x + 1) is set
v . (x + 1) is Element of the carrier of V
v is Element of the carrier of V
(v . x) + 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 . x),v) is Element of the carrier of V
I . (x + 1) is Element of the carrier of V
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . x is Element of the carrier of V
I . x is Element of the carrier of V
x + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . (x + 1) is Element of the carrier of V
I . (x + 1) is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence of the carrier of V
(V,(<*> the carrier of 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
[:NAT, the carrier of V:] is Relation-like V38() set
bool [:NAT, the carrier of V:] is V38() set
len (<*> the carrier of V) 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
w is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
w . (len (<*> the carrier of V)) is Element of the carrier of V
w . 0 is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
[:NAT, the carrier of V:] is Relation-like V38() set
bool [:NAT, the carrier of V:] is V38() set
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like Element of bool [:NAT, the carrier of V:]
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,v) is Element of the carrier of V
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence 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 Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len w) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
dom w is Element of bool NAT
w | (dom w) is Relation-like NAT -defined dom w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
w . (len w) is set
(V,w) is Element of the carrier of V
(V,w) is Element of the carrier of V
(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 . ((V,w),v) is Element of the carrier of V
[:NAT, the carrier of V:] is Relation-like V38() set
bool [:NAT, the carrier of V:] is V38() set
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
v . (len w) is Element of the carrier of V
v . 0 is Element of the carrier of V
I is Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
I . (len w) is Element of the carrier of V
I . 0 is Element of the carrier of V
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg x is V38() x -element Element of bool NAT
w | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (x + 1) is non empty V38() x + 1 -element Element of bool NAT
w | (Seg (x + 1)) is Relation-like NAT -defined Seg (x + 1) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
dom w is Element of bool NAT
w . (x + 1) is set
Seg (len w) is V38() len w -element Element of bool NAT
n is Element of the carrier of V
w . (x + 1) is set
m2 is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
m2 | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
m2 is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v . (x + 1) is Element of the carrier of V
v . x is Element of the carrier of V
(v . x) + n is Element of the carrier of V
the addF of V . ((v . x),n) is Element of the carrier of V
I . (x + 1) is Element of the carrier of V
I . x is Element of the carrier of V
(I . x) + n is Element of the carrier of V
the addF of V . ((I . x),n) is Element of the carrier of V
len m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (len v) is Element of the carrier of V
v . (len v) is Element of the carrier of V
x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg x is V38() x -element Element of bool NAT
w | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (x + 1) is non empty V38() x + 1 -element Element of bool NAT
w | (Seg (x + 1)) is Relation-like NAT -defined Seg (x + 1) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
I . (len v) is Element of the carrier of V
v . (len v) is Element of the carrier of V
Seg 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 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
w | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined the carrier of V -valued 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
x is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (len x) is Element of the carrier of V
v . (len x) is Element of the carrier of V
I . (len w) is 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
w is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
dom w is Element of bool NAT
(v,w) is right_complementable Element of the carrier of v
w is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(v,w) is right_complementable Element of the carrier of v
(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,(v,w)) is set
Seg (len w) is V38() len w -element Element of bool NAT
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len I) is V38() len I -element Element of bool NAT
Seg v is V38() v -element Element of bool NAT
I | (Seg v) is Relation-like NAT -defined Seg v -defined NAT -defined the carrier of v -valued Function-like FinSubsequence-like set
x | (Seg v) is Relation-like NAT -defined Seg v -defined NAT -defined the carrier of v -valued Function-like FinSubsequence-like set
n is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len v) is V38() len v -element Element of bool NAT
dom v is Element of bool NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
m2 is right_complementable Element of the carrier of v
n . m2 is set
dom n is Element of bool NAT
x . m2 is set
I . m2 is set
(v,m2,V) is right_complementable Element of the carrier of v
the of v . (V,m2) is set
v . m2 is set
dom I is Element of bool NAT
dom x is Element of bool NAT
I . (v + 1) is set
x . (v + 1) is set
m2 is right_complementable Element of the carrier of v
m2 is right_complementable Element of the carrier of v
(v,m2,V) is right_complementable Element of the carrier of v
the of v . (V,m2) is set
Seg (len n) is V38() len n -element Element of bool NAT
(v,I) is right_complementable Element of the carrier of v
(v,v) is right_complementable Element of the carrier of v
(v,(v,v),m2) 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),m2) is right_complementable Element of the carrier of v
(v,n) is right_complementable Element of the carrier of v
(v,(v,n),V) is right_complementable Element of the carrier of v
the of v . (V,(v,n)) is set
(v,(v,(v,n),V),(v,m2,V)) is right_complementable Element of the carrier of v
the addF of v . ((v,(v,n),V),(v,m2,V)) is right_complementable Element of the carrier of v
(v,(v,n),m2) is right_complementable Element of the carrier of v
the addF of v . ((v,n),m2) is right_complementable Element of the carrier of v
(v,(v,(v,n),m2),V) is right_complementable Element of the carrier of v
the of v . (V,(v,(v,n),m2)) is set
(v,x) is right_complementable Element of the carrier of v
(v,(v,x),V) is right_complementable Element of the carrier of v
the of v . (V,(v,x)) is set
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len I) is V38() len I -element Element of bool NAT
(v,I) is right_complementable Element of the carrier of v
(v,x) is right_complementable Element of the carrier of v
(v,(v,x),V) is right_complementable Element of the carrier of v
the of v . (V,(v,x)) is set
v is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len v) is V38() len v -element Element of bool NAT
(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,I) is right_complementable Element of the carrier of v
(v,(v,I),V) is right_complementable Element of the carrier of v
the of v . (V,(v,I)) is set
v is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of v -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len v) is V38() len v -element Element of bool NAT
(v,v) is right_complementable Element of the carrier of v
(v,I) is right_complementable Element of the carrier of v
(v,(v,I),V) is right_complementable Element of the carrier of v
the of v . (V,(v,I)) is set
V is non empty right_complementable () () () addLoopStr
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
dom v is Element of bool NAT
(V,v) is right_complementable Element of the carrier of V
(V,w) is right_complementable Element of the carrier of V
- (V,w) is right_complementable Element of the carrier of V
Seg (len v) is V38() len v -element Element of bool NAT
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len v) is V38() len v -element Element of bool NAT
Seg w is V38() w -element Element of bool NAT
v | (Seg w) is Relation-like NAT -defined Seg w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
I | (Seg w) is Relation-like NAT -defined Seg w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
x is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len x) is V38() len x -element Element of bool NAT
dom x is Element of bool NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
m2 is right_complementable Element of the carrier of V
v . n is set
dom v is Element of bool NAT
I . n is set
v . n is set
- m2 is right_complementable Element of the carrier of V
x . n is set
dom v is Element of bool NAT
dom I is Element of bool NAT
v . (w + 1) is set
I . (w + 1) is set
n is right_complementable Element of the carrier of V
m2 is right_complementable Element of the carrier of V
- m2 is right_complementable Element of the carrier of V
Seg (len v) is V38() len v -element Element of bool NAT
(V,v) is right_complementable Element of the carrier of V
(V,x) is right_complementable Element of the carrier of V
(V,(V,x),n) 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,x),n) is right_complementable Element of the carrier of V
(V,v) is right_complementable Element of the carrier of V
- (V,v) is right_complementable Element of the carrier of V
(V,(- (V,v)),(- m2)) is right_complementable Element of the carrier of V
the addF of V . ((- (V,v)),(- m2)) is right_complementable Element of the carrier of V
(V,(V,v),m2) is right_complementable Element of the carrier of V
the addF of V . ((V,v),m2) is right_complementable Element of the carrier of V
- (V,(V,v),m2) is right_complementable Element of the carrier of V
(V,I) is right_complementable Element of the carrier of V
- (V,I) is right_complementable Element of the carrier of V
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len v) is V38() len v -element Element of bool NAT
(V,v) is right_complementable Element of the carrier of V
(V,I) is right_complementable Element of the carrier of V
- (V,I) is right_complementable Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len w) is V38() len w -element Element of bool NAT
(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
(V,v) is right_complementable Element of the carrier of V
- (V,v) is right_complementable Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len w) is V38() len w -element Element of bool NAT
(V,w) is right_complementable Element of the carrier of V
(V,v) is right_complementable Element of the carrier of V
- (V,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 Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v ^ w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,(v ^ w)) is Element of the carrier of V
(V,v) is Element of the carrier of V
(V,w) is Element of the carrier of V
(V,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,v),(V,w)) is Element of the carrier of V
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v ^ v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,(v ^ v)) is Element of the carrier of V
(V,v) is Element of the carrier of V
(V,v) + (V,v) is Element of the carrier of V
the addF of V . ((V,v),(V,v)) is Element of the carrier of V
Seg w is V38() w -element Element of bool NAT
v | (Seg w) is Relation-like NAT -defined Seg w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
rng v is set
dom v is Element of bool NAT
Seg (w + 1) is non empty V38() w + 1 -element Element of bool NAT
v . (w + 1) is set
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom I is Element of bool NAT
I . v is set
v . v is set
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len I) is V38() len I -element Element of bool NAT
v ^ I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (v ^ I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len (v ^ I)) is V38() len (v ^ I) -element Element of bool NAT
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len v) + (len I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg ((len v) + (len I)) is V38() (len v) + (len I) -element Element of bool NAT
dom (v ^ v) is Element of bool NAT
len (v ^ v) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (len (v ^ v)) is V38() len (v ^ v) -element Element of bool NAT
(len v) + (len v) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg ((len v) + (len v)) is V38() (len v) + (len v) -element Element of bool NAT
dom (v ^ I) is Element of bool NAT
v is set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
dom v is Element of bool NAT
Seg (len v) is V38() len v -element Element of bool NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(len v) + m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len v) + w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(v ^ I) . n is set
I . m2 is set
(v ^ v) . n is set
v . m2 is set
(v ^ I) . v is set
(v ^ v) . v is set
v . n is set
(dom (v ^ v)) /\ (Seg (len (v ^ I))) is Element of bool NAT
(v ^ v) | (Seg (len (v ^ I))) is Relation-like NAT -defined Seg (len (v ^ I)) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
(v ^ v) | (dom (v ^ I)) is Relation-like NAT -defined dom (v ^ I) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
x is Element of the carrier of V
<*x*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom <*x*> is non empty trivial 1 -element Element of bool NAT
(len I) + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . ((len I) + v) is set
<*x*> . v is set
len <*x*> is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len I) + (len <*x*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg ((len I) + (len <*x*>)) is non empty V38() (len I) + (len <*x*>) -element Element of bool NAT
I ^ <*x*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(v ^ I) ^ <*x*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(len (v ^ I)) + (len <*x*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len (v ^ I)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(v ^ v) . ((len v) + (len v)) is set
(v ^ v) . (len (v ^ v)) is set
(V,(v ^ I)) is Element of the carrier of V
(V,(v ^ I)) + x is Element of the carrier of V
the addF of V . ((V,(v ^ I)),x) is Element of the carrier of V
(V,I) is Element of the carrier of V
(V,v) + (V,I) is Element of the carrier of V
the addF of V . ((V,v),(V,I)) is Element of the carrier of V
((V,v) + (V,I)) + x is Element of the carrier of V
the addF of V . (((V,v) + (V,I)),x) is Element of the carrier of V
(V,I) + x is Element of the carrier of V
the addF of V . ((V,I),x) is Element of the carrier of V
(V,v) + ((V,I) + x) is Element of the carrier of V
the addF of V . ((V,v),((V,I) + x)) is Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v ^ w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,(v ^ w)) is Element of the carrier of V
(V,w) is Element of the carrier of V
(V,v) + (V,w) is Element of the carrier of V
the addF of V . ((V,v),(V,w)) is Element of the carrier of V
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence 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
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
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 Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v*>) is right_complementable Element of the carrier of V
[:NAT, the carrier of V:] is Relation-like V38() set
bool [:NAT, the carrier of V:] is V38() set
len <*v*> is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
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 Relation-like NAT -defined the carrier of V -valued Function-like V18( NAT , the carrier of V) Element of bool [:NAT, the carrier of V:]
w . (len <*v*>) is right_complementable Element of the carrier of V
w . 0 is right_complementable Element of the carrier of V
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v + 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) is set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
<*v*> . (0 + 1) is set
w . 1 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 () () () addLoopStr
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is set
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng w is set
(V,v) is Element of the carrier of V
(V,w) is Element of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
rng v is set
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng I is set
Seg (w + 1) is non empty V38() w + 1 -element Element of bool NAT
dom v is Element of bool NAT
v . (w + 1) is set
dom I is Element of bool NAT
x is set
I . x is set
len I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
n + m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
m2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg m2 is V38() m2 -element Element of bool NAT
q2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
n + q2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + q2) is set
q2 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
dom q2 is Element of bool NAT
rng q2 is set
p is set
m1 is set
q2 . m1 is set
q1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
n + q1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + q1) is set
q2 is Element of the carrier of V
Seg w is V38() w -element Element of bool NAT
v | (Seg w) is Relation-like NAT -defined Seg w -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
p is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{(w + 1)} is non empty trivial 1 -element set
(Seg (w + 1)) \ {(w + 1)} is Element of bool NAT
v .: (Seg w) is set
v .: (Seg (w + 1)) is set
Im (v,(w + 1)) is set
v .: {(w + 1)} is set
(v .: (Seg (w + 1))) \ (Im (v,(w + 1))) is Element of bool (v .: (Seg (w + 1)))
bool (v .: (Seg (w + 1))) is set
m1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
1 + m1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg m1 is V38() m1 -element Element of bool NAT
I | (Seg m1) is Relation-like NAT -defined Seg m1 -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set
q1 is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len q1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
q2 is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom q2 is Element of bool NAT
v is Element of the carrier of V
<*v*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
q1 ^ <*v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (q1 ^ <*v*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
len <*v*> is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
m1 + (len <*v*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len (q1 ^ <*v*>)) + q is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . ((len (q1 ^ <*v*>)) + q) is set
q2 . q is set
q1 ^ q2 is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{v} is non empty trivial 1 -element set
rng (q1 ^ q2) is set
{v} /\ (rng (q1 ^ q2)) is set
the Element of {v} /\ (rng (q1 ^ q2)) is Element of {v} /\ (rng (q1 ^ q2))
rng q1 is set
dom q1 is Element of bool NAT
y2 is set
q1 . y2 is set
x1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q1 . x1 is set
I . x1 is set
I . n is set
rng q2 is set
y2 is set
q2 . y2 is set
x1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
n + x1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + x1) is set
(rng q1) \/ (rng q2) is set
j is set
dom (q1 ^ q2) is set
y2 is set
(q1 ^ q2) . j is set
(q1 ^ q2) . y2 is set
dom (q1 ^ q2) is Element of bool NAT
x1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(len q1) + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 . j is set
n + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + j) is set
x2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
j2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(len q1) + j2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 . j2 is set
n + j2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + j2) is set
m1 + j2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(q1 ^ q2) . (m1 + j2) is set
dom q1 is Element of bool NAT
q1 . x2 is set
I . x2 is set
(q1 ^ q2) . x2 is set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(len q1) + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 . j is set
n + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + j) is set
q1 . x1 is set
I . x1 is set
(q1 ^ q2) . x1 is set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
(len q1) + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
q2 . j is set
n + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
I . (n + j) is set
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
dom <*v*> is non empty trivial 1 -element Element of bool NAT
(len p) + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . ((len p) + j) is set
<*v*> . j is set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
dom (q1 ^ <*v*>) is non empty Element of bool NAT
dom q1 is Element of bool NAT
q1 . j is set
I . j is set
(q1 ^ <*v*>) . j is set
(len q1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(q1 ^ <*v*>) . ((len q1) + 1) is set
<*v*> . 1 is set
{n} is non empty trivial 1 -element set
m1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg (m1 + 1) is non empty V38() m1 + 1 -element Element of bool NAT
(Seg m1) \/ {n} is non empty set
len q2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len (q1 ^ <*v*>)) + (len q2) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(len q1) + (len <*v*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
((len q1) + (len <*v*>)) + m2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
Seg ((len (q1 ^ <*v*>)) + (len q2)) is non empty V38() (len (q1 ^ <*v*>)) + (len q2) -element Element of bool NAT
(q1 ^ <*v*>) ^ q2 is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (q1 ^ <*v*>) is non empty set
rng q2 is set
(rng (q1 ^ <*v*>)) \/ (rng q2) is non empty set
rng <*v*> is non empty trivial 1 -element set
rng q1 is set
(rng <*v*>) \/ (rng q1) is non empty set
((rng <*v*>) \/ (rng q1)) \/ (rng q2) is non empty set
{v} \/ (rng q1) is non empty set
({v} \/ (rng q1)) \/ (rng q2) is non empty set
(rng q1) \/ (rng q2) is set
{v} \/ ((rng q1) \/ (rng q2)) is non empty set
{v} \/ (rng (q1 ^ q2)) is non empty set
(rng I) \ {v} is Element of bool (rng I)
bool (rng I) is set
rng p is set
dom p is Element of bool NAT
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal set
v . j is set
p . j is set
p ^ <*v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,v) is Element of the carrier of V
(V,p) is Element of the carrier of V
(V,<*v*>) is Element of the carrier of V
(V,(V,p),(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,p),(V,<*v*>)) is Element of the carrier of V
(V,I) is Element of the carrier of V
(V,(q1 ^ <*v*>)) is Element of the carrier of V
(V,q2) is Element of the carrier of V
(V,(V,(q1 ^ <*v*>)),(V,q2)) is Element of the carrier of V
the addF of V . ((V,(q1 ^ <*v*>)),(V,q2)) is Element of the carrier of V
(V,q1) is Element of the carrier of V
(V,(V,q1),(V,<*v*>)) is Element of the carrier of V
the addF of V . ((V,q1),(V,<*v*>)) is Element of the carrier of V
(V,(V,(V,q1),(V,<*v*>)),(V,q2)) is Element of the carrier of V
the addF of V . ((V,(V,q1),(V,<*v*>)),(V,q2)) is Element of the carrier of V
(V,(V,q1),(V,q2)) is Element of the carrier of V
the addF of V . ((V,q1),(V,q2)) is Element of the carrier of V
(V,(V,<*v*>),(V,(V,q1),(V,q2))) is Element of the carrier of V
the addF of V . ((V,<*v*>),(V,(V,q1),(V,q2))) is Element of the carrier of V
(V,(q1 ^ q2)) is Element of the carrier of V
(V,(V,(q1 ^ q2)),(V,<*v*>)) is Element of the carrier of V
the addF of V . ((V,(q1 ^ q2)),(V,<*v*>)) is Element of the carrier of V
w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
w + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
rng v is set
I is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng I is set
(V,v) is Element of the carrier of V
(V,I) is Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
rng w is set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is set
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,w) 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,v) is Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
rng w is set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is set
(V,w) is Element of the carrier of V
(V,v) is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence of the carrier of V
(V,(<*> the carrier of 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 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 Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier 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
<*v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*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 Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*v*> ^ <*w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence 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*>) is right_complementable Element of the carrier of V
(V,<*w*>) is right_complementable Element of the carrier of V
(V,<*v*>) + (V,<*w*>) is right_complementable Element of the carrier of V
the addF of V . ((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 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
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,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) + 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 Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*v,w*> ^ <*w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,<*v,w*>) is right_complementable Element of the carrier of V
(V,<*w*>) is right_complementable Element of the carrier of V
(V,<*v,w*>) + (V,<*w*>) is right_complementable Element of the carrier of V
the addF of V . ((V,<*v,w*>),(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,<*v,w*>),w) is right_complementable Element of the carrier of V
V is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence of the carrier of V
(V,(<*> the carrier of V)) is right_complementable Element of the carrier of V
v is ext-real V36() real Element of REAL
(V,(V,(<*> the carrier of V)),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,(V,(<*> the carrier of 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 is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
v is ext-real V36() real Element of REAL
w is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
<*w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,w*>) is right_complementable Element of the carrier of V
(V,(V,<*w,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,(V,<*w,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
the of V . (v,w) is set
(V,(V,w,v),(V,w,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,w,v),(V,w,v)) 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 . (w,w) is right_complementable Element of the carrier of V
(V,(V,w,w),v) is right_complementable Element of the carrier of V
the of V . (v,(V,w,w)) is set
V is non empty right_complementable () () () () () () () ()
the carrier of V is non empty set
v is ext-real V36() real Element of REAL
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,w,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,w,v*>) is right_complementable Element of the carrier of V
(V,(V,<*w,w,v*>),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,(V,<*w,w,v*>)) 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
the of V . (v,w) is set
(V,(V,w,v),(V,w,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,w,v),(V,w,v)) is right_complementable Element of the carrier of V
(V,v,v) is right_complementable Element of the carrier of V
the of V . (v,v) is set
(V,(V,(V,w,v),(V,w,v)),(V,v,v)) is right_complementable Element of the carrier of V
the addF of V . ((V,(V,w,v),(V,w,v)),(V,v,v)) 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 . (w,w) is right_complementable Element of the carrier of V
(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
(V,(V,(V,w,w),v),v) is right_complementable Element of the carrier of V
the of V . (v,(V,(V,w,w),v)) is set
(V,(V,w,w),v) is right_complementable Element of the carrier of V
the of V . (v,(V,w,w)) is set
(V,(V,(V,w,w),v),(V,v,v)) is right_complementable Element of the carrier of V
the addF of V . ((V,(V,w,w),v),(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
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence of the carrier of V
(V,(<*> the carrier of V)) is right_complementable Element of the carrier of V
- (V,(<*> the carrier of 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) 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 Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*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 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 Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier 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
- v 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,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) 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
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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 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) - 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,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,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,(V,v,w),w) is right_complementable Element of the carrier of V
- (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
(- (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 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 Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w*>) is right_complementable Element of the carrier of V
<*w,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,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 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 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 Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v*>) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
<*v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w*>) is right_complementable Element of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w*>) is right_complementable Element of the carrier of V
(V,<*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,<*v*>),(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 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 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 Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(0. V),v*>) is right_complementable Element of the carrier of V
<*v,(0. V)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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 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 + (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 is right_complementable Element of the carrier of V
<*v,(- v)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(- v)*>) is right_complementable Element of the carrier of V
<*(- v),v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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 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
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
<*v,(- w)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(- w)*>) is right_complementable Element of the carrier of V
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 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
<*(- v),(- w)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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 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 right_complementable Element of the carrier of V
- (w + 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 . ((- 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
v is right_complementable Element of the carrier of V
<*v,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,v*>) is right_complementable Element of the carrier of V
(V,v,2) 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 . (2,v) is set
(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 . (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
- 2 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)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(- v),(- v)*>) is right_complementable Element of the carrier of V
(V,v,(- 2)) 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 . ((- 2),v) is set
(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,v) is right_complementable Element of the carrier of V
<*v,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,v*>) is right_complementable Element of the carrier of V
- (V,<*v,v*>) is right_complementable Element of the carrier of V
(V,v,2) is right_complementable Element of the carrier of V
the of V . (2,v) is set
- (V,v,2) is right_complementable Element of the carrier of V
(V,(V,v,2),(- 1)) is right_complementable Element of the carrier of V
the of V . ((- 1),(V,v,2)) is set
(- 1) * 2 is ext-real non positive V36() real Element of REAL
(V,v,((- 1) * 2)) is right_complementable Element of the carrier of V
the of V . (((- 1) * 2),v) 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
<*v*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v*>) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w*>) is right_complementable Element of the carrier of V
(V,<*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,<*v*>),(V,<*w*>)) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,w*>) is right_complementable Element of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w*>) is right_complementable Element of the carrier of V
((V,<*v*>) + (V,<*w*>)) + (V,<*w*>) is right_complementable Element of the carrier of V
the addF of V . (((V,<*v*>) + (V,<*w*>)),(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
the addF of V . ((v + w),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*>) + 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,<*v*>) + w) + (V,<*w*>) is right_complementable Element of the carrier of V
the addF of V . (((V,<*v*>) + w),(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 Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w*>) is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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 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,w*>),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
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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w*>) is right_complementable Element of the carrier of V
(V,(V,<*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 . ((V,<*v,w*>),w) is right_complementable Element of the carrier of V
(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,w,v),w) is right_complementable Element of the carrier of V
the addF of V . ((V,w,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,w) is right_complementable Element of the carrier of V
(V,w,(V,v,w)) is right_complementable Element of the carrier of V
the addF of V . (w,(V,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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,w*>) is right_complementable Element of the carrier of V
(V,(V,<*w,w*>),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,<*w,w*>),v) is right_complementable Element of the carrier of V
(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,w,v),w) is right_complementable Element of the carrier of V
the addF of V . ((V,w,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 . (w,w) is right_complementable Element of the carrier of V
(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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*w,w,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,w,v*>) is right_complementable Element of the carrier of V
(V,w,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 . (w,v) is right_complementable Element of the carrier of V
(V,(V,w,v),w) is right_complementable Element of the carrier of V
the addF of V . ((V,w,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 . (w,w) is right_complementable Element of the carrier of V
(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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,w*>) is right_complementable Element of the carrier of V
(V,w,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 . (w,v) is right_complementable Element of the carrier of V
(V,(V,w,v),w) is right_complementable Element of the carrier of V
the addF of V . ((V,w,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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,w*>) is right_complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(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
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,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*w,v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,v,w*>) is right_complementable Element of the carrier of V
<*w,w,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*w,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
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),(0. V),v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(0. V),(0. V),v*>) is right_complementable Element of the carrier of V
<*(0. V),v,(0. V)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(0. V),v,(0. V)*>) is right_complementable Element of the carrier of V
<*v,(0. V),(0. V)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(0. 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
((0. V) + (0. V)) + v is right_complementable Element of the carrier of V
the addF of V . (((0. V) + (0. 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
((0. V) + v) + (0. V) is right_complementable Element of the carrier of V
the addF of V . (((0. 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 + (0. V)) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((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
w is right_complementable Element of the carrier of V
<*(0. V),v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(0. V),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,(0. V)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,(0. V)*>) is right_complementable Element of the carrier of V
<*v,(0. V),w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(0. V),w*>) 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
((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
(v + w) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((v + w),(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 + (0. V)) + w is right_complementable Element of the carrier of V
the addF of V . ((v + (0. 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
v is right_complementable Element of the carrier of V
<*v,v,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,v,v*>) is right_complementable Element of the carrier of V
(V,v,3) 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 . (3,v) is set
<*v,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,v*>) is right_complementable Element of the carrier of V
(V,(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,v*>),v) is right_complementable Element of the carrier of V
(V,v,2) is right_complementable Element of the carrier of V
the of V . (2,v) is set
(V,(V,v,2),v) is right_complementable Element of the carrier of V
the addF of V . ((V,v,2),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 . (1,v) is set
(V,(V,v,2),(V,v,1)) is right_complementable Element of the carrier of V
the addF of V . ((V,v,2),(V,v,1)) is right_complementable Element of the carrier of V
2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,v,(2 + 1)) is right_complementable Element of the carrier of V
the of V . ((2 + 1),v) is set
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(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 Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
(V,v) is right_complementable Element of the carrier of V
v . 1 is set
dom v is Element of bool NAT
rng v is set
w is right_complementable Element of the carrier of V
<*w*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty trivial V38() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . 1 is set
v . 2 is set
(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 + 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,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
V is non empty right_complementable () () addLoopStr
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() real V38() cardinal Element of NAT
v . 1 is set
v . 2 is set
v . 3 is set
(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 + 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 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
<*w,w,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
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
V is non empty addLoopStr
the carrier of V is non empty 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
(0. V) + v is Element of the carrier of V
the addF of V . ((0. V),v) is 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
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 + v is Element of the carrier of V
the addF of V . (w,v) is Element of the carrier of V
V is ext-real V36() real set
- V is ext-real V36() real set
v is non empty left_complementable right_complementable complementable () () () () () () () () ()
the carrier of v is non empty set
w is left_complementable right_complementable complementable Element of the carrier of v
(v,w,(- V)) is left_complementable right_complementable 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 left_complementable right_complementable complementable Element of the carrier of v
the of v . (V,w) is set
- (v,w,V) is left_complementable right_complementable complementable Element of the carrier of v
- w is left_complementable right_complementable complementable Element of the carrier of v
(v,(- w),V) is left_complementable right_complementable complementable Element of the carrier of v
the of v . (V,(- w)) is set
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
<*> the carrier of V is Relation-like non-empty empty-yielding NAT -defined the carrier of V -valued 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 FinSequence of the carrier of V
(V,(<*> the carrier of V)) is left_complementable right_complementable complementable Element of the carrier of V
- (V,(<*> the carrier of V)) is left_complementable right_complementable complementable Element of the carrier of V
0. V is V57(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
- (0. V) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
v is left_complementable right_complementable complementable Element of the carrier of V
w is left_complementable right_complementable complementable Element of the carrier of V
<*v,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w*>) is left_complementable right_complementable complementable Element of the carrier of V
- (V,<*v,w*>) is left_complementable right_complementable complementable Element of the carrier of V
- v is left_complementable right_complementable complementable Element of the carrier of V
(- v) - w is left_complementable right_complementable complementable Element of the carrier of V
- w is left_complementable right_complementable complementable Element of the carrier of V
(- v) + (- w) is 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_complementable right_complementable complementable Element of the carrier of V
(V,v,w) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (v,w) is left_complementable right_complementable complementable Element of the carrier of V
- (V,v,w) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
v is left_complementable right_complementable complementable Element of the carrier of V
w is left_complementable right_complementable complementable Element of the carrier of V
w is left_complementable right_complementable complementable Element of the carrier of V
<*v,w,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,w,w*>) is left_complementable right_complementable complementable Element of the carrier of V
- (V,<*v,w,w*>) is left_complementable right_complementable complementable Element of the carrier of V
- v is left_complementable right_complementable complementable Element of the carrier of V
(- v) - w is left_complementable right_complementable complementable Element of the carrier of V
- w is left_complementable right_complementable complementable Element of the carrier of V
(- v) + (- w) is 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_complementable right_complementable complementable Element of the carrier of V
((- v) - w) - w is left_complementable right_complementable complementable Element of the carrier of V
- w is left_complementable right_complementable complementable Element of the carrier of V
((- v) - w) + (- w) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (((- v) - w),(- w)) is left_complementable right_complementable complementable Element of the carrier of V
(V,v,w) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (v,w) is left_complementable right_complementable complementable Element of the carrier of V
(V,(V,v,w),w) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((V,v,w),w) is left_complementable right_complementable complementable Element of the carrier of V
- (V,(V,v,w),w) is left_complementable right_complementable complementable Element of the carrier of V
- (V,v,w) is left_complementable right_complementable complementable Element of the carrier of V
(- (V,v,w)) - w is left_complementable right_complementable complementable Element of the carrier of V
(- (V,v,w)) + (- w) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((- (V,v,w)),(- w)) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
0. V is V57(V) left_complementable right_complementable complementable Element of the carrier of V
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
v is left_complementable right_complementable complementable Element of the carrier of V
- v is left_complementable right_complementable complementable Element of the carrier of V
<*v,(- v)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(- v)*>) is left_complementable right_complementable complementable Element of the carrier of V
<*(- v),v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(- v),v*>) is left_complementable right_complementable complementable Element of the carrier of V
(V,v,(- v)) is 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,(- v)) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
v is left_complementable right_complementable complementable Element of the carrier of V
w is left_complementable right_complementable complementable Element of the carrier of V
- w is left_complementable right_complementable complementable Element of the carrier of V
<*v,(- w)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*v,(- w)*>) is left_complementable right_complementable complementable Element of the carrier of V
v - w is left_complementable right_complementable complementable Element of the carrier of V
v + (- w) is 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_complementable right_complementable complementable Element of the carrier of V
<*(- w),v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(- w),v*>) is left_complementable right_complementable complementable Element of the carrier of V
(V,v,(- w)) is left_complementable right_complementable complementable Element of the carrier of V
V is non empty left_complementable right_complementable complementable () () () () addLoopStr
the carrier of V is non empty set
v is left_complementable right_complementable complementable Element of the carrier of V
- v is left_complementable right_complementable complementable Element of the carrier of V
w is left_complementable right_complementable complementable Element of the carrier of V
- w is left_complementable right_complementable complementable Element of the carrier of V
<*(- v),(- w)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(- v),(- w)*>) is left_complementable right_complementable complementable Element of the carrier of V
(V,v,w) is 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_complementable right_complementable complementable Element of the carrier of V
- (V,v,w) is left_complementable right_complementable complementable Element of the carrier of V
<*(- w),(- v)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,<*(- w),(- v)*>) is left_complementable right_complementable complementable Element of the carrier of V
(V,(- v),(- w)) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((- v),(- w)) is left_complementable right_complementable complementable Element of the carrier of V