:: 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