:: CLVECT_1 semantic presentation

REAL is non empty V50() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty V50() set
COMPLEX is non empty V50() set
omega is non empty epsilon-transitive epsilon-connected ordinal V50() cardinal limit_cardinal set
bool omega is non empty V50() set
bool NAT is non empty V50() set
[:NAT,REAL:] is non empty V50() set
bool [:NAT,REAL:] is non empty V50() set
{} is set
the functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V50() cardinal {} -element FinSequence-membered set is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V50() cardinal {} -element FinSequence-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal Element of NAT
{{},1} is set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V50() cardinal Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
1r is complex Element of COMPLEX
|.1r.| is complex real ext-real Element of REAL
{{}} is 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 non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is 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 :] 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 :]
[:COMPLEX, the non empty set :] is non empty V50() set
[:[:COMPLEX, the non empty set :], the non empty set :] is non empty V50() set
bool [:[:COMPLEX, the non empty set :], the non empty set :] is non empty V50() set
the Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like V18([:COMPLEX, the non empty set :], the non empty set ) Element of bool [:[:COMPLEX, the non empty set :], the non empty set :] is Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like V18([:COMPLEX, the non empty set :], the non empty set ) Element of bool [:[:COMPLEX, 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 [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like V18([:COMPLEX, the non empty set :], the non empty set ) Element of bool [:[:COMPLEX, 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 [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like V18([:COMPLEX, the non empty set :], the non empty set ) Element of bool [:[:COMPLEX, the non empty set :], the non empty set :]) is set
V is non empty ()
the carrier of V is non empty set
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
X is complex set
niltonil is Element of the carrier of V
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
z is complex Element of COMPLEX
[z,niltonil] is Element of [:COMPLEX, the carrier of V:]
{z,niltonil} is set
{z} is non empty trivial 1 -element set
{{z,niltonil},{z}} is set
the of V . [z,niltonil] is Element of the carrier of V
V is non empty set
[:V,V:] is non empty set
[:[:V,V:],V:] is non empty set
bool [:[:V,V:],V:] is non empty set
[:COMPLEX,V:] is non empty V50() set
[:[:COMPLEX,V:],V:] is non empty V50() set
bool [:[:COMPLEX,V:],V:] is non empty V50() set
niltonil is Element of V
X is Relation-like [:V,V:] -defined V -valued Function-like V18([:V,V:],V) Element of bool [:[:V,V:],V:]
z is Relation-like [:COMPLEX,V:] -defined V -valued Function-like V18([:COMPLEX,V:],V) Element of bool [:[:COMPLEX,V:],V:]
(V,niltonil,X,z) is () ()
op0 is epsilon-transitive epsilon-connected ordinal 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 (COMPLEX,1) is Relation-like [:COMPLEX,1:] -defined 1 -valued Function-like V18([:COMPLEX,1:],1) Element of bool [:[:COMPLEX,1:],1:]
[:COMPLEX,1:] is non empty V50() set
[:[:COMPLEX,1:],1:] is non empty V50() set
bool [:[:COMPLEX,1:],1:] is non empty V50() set
(1,op0,op2,(pr2 (COMPLEX,1))) is non empty () ()
() is () ()
the carrier of () is set
{0} is non empty trivial 1 -element Element of bool NAT
V is non empty trivial V68() 1 -element () ()
the carrier of V is non empty trivial V50() 1 -element set
niltonil is Element of the carrier of V
X is Element of the carrier of V
niltonil + 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,X) is Element of the carrier of V
[niltonil,X] is set
{niltonil,X} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,X},{niltonil}} is set
the addF of V . [niltonil,X] is set
X + niltonil is Element of the carrier of V
the addF of V . (X,niltonil) is Element of the carrier of V
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the addF of V . [X,niltonil] is set
the carrier of V is non empty trivial V50() 1 -element set
niltonil is Element of the carrier of V
X is Element of the carrier of V
niltonil + 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,X) is Element of the carrier of V
[niltonil,X] is set
{niltonil,X} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,X},{niltonil}} is set
the addF of V . [niltonil,X] is set
z is Element of the carrier of V
(niltonil + X) + z is Element of the carrier of V
the addF of V . ((niltonil + X),z) is Element of the carrier of V
[(niltonil + X),z] is set
{(niltonil + X),z} is set
{(niltonil + X)} is non empty trivial 1 -element set
{{(niltonil + X),z},{(niltonil + X)}} is set
the addF of V . [(niltonil + X),z] is set
X + z is Element of the carrier of V
the addF of V . (X,z) is Element of the carrier of V
[X,z] is set
{X,z} is set
{X} is non empty trivial 1 -element set
{{X,z},{X}} is set
the addF of V . [X,z] is set
niltonil + (X + z) is Element of the carrier of V
the addF of V . (niltonil,(X + z)) is Element of the carrier of V
[niltonil,(X + z)] is set
{niltonil,(X + z)} is set
{{niltonil,(X + z)},{niltonil}} is set
the addF of V . [niltonil,(X + z)] is set
the carrier of V is non empty trivial V50() 1 -element set
niltonil is Element of the carrier of V
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
niltonil + (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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,(0. V)) is Element of the carrier of V
[niltonil,(0. V)] is set
{niltonil,(0. V)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(0. V)},{niltonil}} is set
the addF of V . [niltonil,(0. V)] is set
the carrier of V is non empty trivial V50() 1 -element set
niltonil is Element of the carrier of V
niltonil + niltonil 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,niltonil) is Element of the carrier of V
[niltonil,niltonil] is set
{niltonil,niltonil} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,niltonil},{niltonil}} is set
the addF of V . [niltonil,niltonil] is set
0. V is zero 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 V50() 1 -element set
X is Element of the carrier of V
z is Element of the carrier of V
X + z 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (X,z) is Element of the carrier of V
[X,z] is set
{X,z} is set
{X} is non empty trivial 1 -element set
{{X,z},{X}} is set
the addF of V . [X,z] is set
niltonil is complex set
(V,(X + z),niltonil) is Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[niltonil,(X + z)] is set
{niltonil,(X + z)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(X + z)},{niltonil}} is set
the of V . [niltonil,(X + z)] is set
(V,X,niltonil) is Element of the carrier of V
[niltonil,X] is set
{niltonil,X} is set
{{niltonil,X},{niltonil}} is set
the of V . [niltonil,X] is set
(V,z,niltonil) is Element of the carrier of V
[niltonil,z] is set
{niltonil,z} is set
{{niltonil,z},{niltonil}} is set
the of V . [niltonil,z] is set
(V,X,niltonil) + (V,z,niltonil) is Element of the carrier of V
the addF of V . ((V,X,niltonil),(V,z,niltonil)) is Element of the carrier of V
[(V,X,niltonil),(V,z,niltonil)] is set
{(V,X,niltonil),(V,z,niltonil)} is set
{(V,X,niltonil)} is non empty trivial 1 -element set
{{(V,X,niltonil),(V,z,niltonil)},{(V,X,niltonil)}} is set
the addF of V . [(V,X,niltonil),(V,z,niltonil)] is set
z is Element of the carrier of V
niltonil is complex set
X is complex set
niltonil + X is complex set
(V,z,(niltonil + X)) is Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[(niltonil + X),z] is set
{(niltonil + X),z} is set
{(niltonil + X)} is non empty trivial 1 -element set
{{(niltonil + X),z},{(niltonil + X)}} is set
the of V . [(niltonil + X),z] is set
(V,z,niltonil) is Element of the carrier of V
[niltonil,z] is set
{niltonil,z} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,z},{niltonil}} is set
the of V . [niltonil,z] is set
(V,z,X) is Element of the carrier of V
[X,z] is set
{X,z} is set
{X} is non empty trivial 1 -element set
{{X,z},{X}} is set
the of V . [X,z] is set
(V,z,niltonil) + (V,z,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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((V,z,niltonil),(V,z,X)) is Element of the carrier of V
[(V,z,niltonil),(V,z,X)] is set
{(V,z,niltonil),(V,z,X)} is set
{(V,z,niltonil)} is non empty trivial 1 -element set
{{(V,z,niltonil),(V,z,X)},{(V,z,niltonil)}} is set
the addF of V . [(V,z,niltonil),(V,z,X)] is set
z is Element of the carrier of V
niltonil is complex set
X is complex set
niltonil * X is complex set
(V,z,(niltonil * X)) is Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[(niltonil * X),z] is set
{(niltonil * X),z} is set
{(niltonil * X)} is non empty trivial 1 -element set
{{(niltonil * X),z},{(niltonil * X)}} is set
the of V . [(niltonil * X),z] is set
(V,z,X) is Element of the carrier of V
[X,z] is set
{X,z} is set
{X} is non empty trivial 1 -element set
{{X,z},{X}} is set
the of V . [X,z] is set
(V,(V,z,X),niltonil) is Element of the carrier of V
[niltonil,(V,z,X)] is set
{niltonil,(V,z,X)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(V,z,X)},{niltonil}} is set
the of V . [niltonil,(V,z,X)] is set
niltonil is Element of the carrier of V
(V,niltonil,1r) is Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[1r,niltonil] is set
{1r,niltonil} is set
{1r} is non empty trivial 1 -element set
{{1r,niltonil},{1r}} is set
the of V . [1r,niltonil] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
niltonil is right_complementable Element of the carrier of V
X is complex set
(V,niltonil,X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
0c is complex Element of COMPLEX
(V,niltonil,0c) is right_complementable Element of the carrier of V
[0c,niltonil] is set
{0c,niltonil} is set
{0c} is non empty trivial 1 -element set
{{0c,niltonil},{0c}} is set
the of V . [0c,niltonil] is set
niltonil + (V,niltonil,0c) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,(V,niltonil,0c)) is right_complementable Element of the carrier of V
[niltonil,(V,niltonil,0c)] is set
{niltonil,(V,niltonil,0c)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(V,niltonil,0c)},{niltonil}} is set
the addF of V . [niltonil,(V,niltonil,0c)] is set
(V,niltonil,1r) is right_complementable Element of the carrier of V
[1r,niltonil] is set
{1r,niltonil} is set
{1r} is non empty trivial 1 -element set
{{1r,niltonil},{1r}} is set
the of V . [1r,niltonil] is set
(V,niltonil,1r) + (V,niltonil,0c) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,1r),(V,niltonil,0c)) is right_complementable Element of the carrier of V
[(V,niltonil,1r),(V,niltonil,0c)] is set
{(V,niltonil,1r),(V,niltonil,0c)} is set
{(V,niltonil,1r)} is non empty trivial 1 -element set
{{(V,niltonil,1r),(V,niltonil,0c)},{(V,niltonil,1r)}} is set
the addF of V . [(V,niltonil,1r),(V,niltonil,0c)] is set
1r + 0c is complex Element of COMPLEX
(V,niltonil,(1r + 0c)) is right_complementable Element of the carrier of V
[(1r + 0c),niltonil] is set
{(1r + 0c),niltonil} is set
{(1r + 0c)} is non empty trivial 1 -element set
{{(1r + 0c),niltonil},{(1r + 0c)}} is set
the of V . [(1r + 0c),niltonil] is set
niltonil + (0. V) is right_complementable Element of the carrier of V
the addF of V . (niltonil,(0. V)) is right_complementable Element of the carrier of V
[niltonil,(0. V)] is set
{niltonil,(0. V)} is set
{{niltonil,(0. V)},{niltonil}} is set
the addF of V . [niltonil,(0. V)] is set
(V,(0. V),X) is right_complementable Element of the carrier of V
[X,(0. V)] is set
{X,(0. V)} is set
{{X,(0. V)},{X}} is set
the of V . [X,(0. V)] is set
(V,(0. V),X) + (V,(0. V),X) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((V,(0. V),X),(V,(0. V),X)) is right_complementable Element of the carrier of V
[(V,(0. V),X),(V,(0. V),X)] is set
{(V,(0. V),X),(V,(0. V),X)} is set
{(V,(0. V),X)} is non empty trivial 1 -element set
{{(V,(0. V),X),(V,(0. V),X)},{(V,(0. V),X)}} is set
the addF of V . [(V,(0. V),X),(V,(0. V),X)] is set
(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
[(0. V),(0. V)] is set
{(0. V),(0. V)} is set
{(0. V)} is non empty trivial 1 -element set
{{(0. V),(0. V)},{(0. V)}} is set
the addF of V . [(0. V),(0. V)] is set
(V,((0. V) + (0. V)),X) is right_complementable Element of the carrier of V
[X,((0. V) + (0. V))] is set
{X,((0. V) + (0. V))} is set
{{X,((0. V) + (0. V))},{X}} is set
the of V . [X,((0. V) + (0. V))] is set
(V,(0. V),X) + (0. V) is right_complementable Element of the carrier of V
the addF of V . ((V,(0. V),X),(0. V)) is right_complementable Element of the carrier of V
[(V,(0. V),X),(0. V)] is set
{(V,(0. V),X),(0. V)} is set
{{(V,(0. V),X),(0. V)},{(V,(0. V),X)}} is set
the addF of V . [(V,(0. V),X),(0. V)] is set
0c is complex Element of COMPLEX
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
niltonil is right_complementable Element of the carrier of V
X is complex set
(V,niltonil,X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
(V,niltonil,1r) is right_complementable Element of the carrier of V
[1r,niltonil] is set
{1r,niltonil} is set
{1r} is non empty trivial 1 -element set
{{1r,niltonil},{1r}} is set
the of V . [1r,niltonil] is set
X " is complex set
(X ") * X is complex set
(V,niltonil,((X ") * X)) is right_complementable Element of the carrier of V
[((X ") * X),niltonil] is set
{((X ") * X),niltonil} is set
{((X ") * X)} is non empty trivial 1 -element set
{{((X ") * X),niltonil},{((X ") * X)}} is set
the of V . [((X ") * X),niltonil] is set
(V,(0. V),(X ")) is right_complementable Element of the carrier of V
[(X "),(0. V)] is set
{(X "),(0. V)} is set
{(X ")} is non empty trivial 1 -element set
{{(X "),(0. V)},{(X ")}} is set
the of V . [(X "),(0. V)] is set
- 1r is complex Element of COMPLEX
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
- niltonil is right_complementable Element of the carrier of V
(V,niltonil,(- 1r)) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[(- 1r),niltonil] is set
{(- 1r),niltonil} is set
{(- 1r)} is non empty trivial 1 -element set
{{(- 1r),niltonil},{(- 1r)}} is set
the of V . [(- 1r),niltonil] is set
niltonil + (V,niltonil,(- 1r)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,(V,niltonil,(- 1r))) is right_complementable Element of the carrier of V
[niltonil,(V,niltonil,(- 1r))] is set
{niltonil,(V,niltonil,(- 1r))} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(V,niltonil,(- 1r))},{niltonil}} is set
the addF of V . [niltonil,(V,niltonil,(- 1r))] is set
(V,niltonil,1r) is right_complementable Element of the carrier of V
[1r,niltonil] is set
{1r,niltonil} is set
{1r} is non empty trivial 1 -element set
{{1r,niltonil},{1r}} is set
the of V . [1r,niltonil] is set
(V,niltonil,1r) + (V,niltonil,(- 1r)) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,1r),(V,niltonil,(- 1r))) is right_complementable Element of the carrier of V
[(V,niltonil,1r),(V,niltonil,(- 1r))] is set
{(V,niltonil,1r),(V,niltonil,(- 1r))} is set
{(V,niltonil,1r)} is non empty trivial 1 -element set
{{(V,niltonil,1r),(V,niltonil,(- 1r))},{(V,niltonil,1r)}} is set
the addF of V . [(V,niltonil,1r),(V,niltonil,(- 1r))] is set
1r + (- 1r) is complex Element of COMPLEX
(V,niltonil,(1r + (- 1r))) is right_complementable Element of the carrier of V
[(1r + (- 1r)),niltonil] is set
{(1r + (- 1r)),niltonil} is set
{(1r + (- 1r))} is non empty trivial 1 -element set
{{(1r + (- 1r)),niltonil},{(1r + (- 1r))}} is set
the of V . [(1r + (- 1r)),niltonil] is set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(- niltonil) + (niltonil + (V,niltonil,(- 1r))) is right_complementable Element of the carrier of V
the addF of V . ((- niltonil),(niltonil + (V,niltonil,(- 1r)))) is right_complementable Element of the carrier of V
[(- niltonil),(niltonil + (V,niltonil,(- 1r)))] is set
{(- niltonil),(niltonil + (V,niltonil,(- 1r)))} is set
{(- niltonil)} is non empty trivial 1 -element set
{{(- niltonil),(niltonil + (V,niltonil,(- 1r)))},{(- niltonil)}} is set
the addF of V . [(- niltonil),(niltonil + (V,niltonil,(- 1r)))] is set
(- niltonil) + niltonil is right_complementable Element of the carrier of V
the addF of V . ((- niltonil),niltonil) is right_complementable Element of the carrier of V
[(- niltonil),niltonil] is set
{(- niltonil),niltonil} is set
{{(- niltonil),niltonil},{(- niltonil)}} is set
the addF of V . [(- niltonil),niltonil] is set
((- niltonil) + niltonil) + (V,niltonil,(- 1r)) is right_complementable Element of the carrier of V
the addF of V . (((- niltonil) + niltonil),(V,niltonil,(- 1r))) is right_complementable Element of the carrier of V
[((- niltonil) + niltonil),(V,niltonil,(- 1r))] is set
{((- niltonil) + niltonil),(V,niltonil,(- 1r))} is set
{((- niltonil) + niltonil)} is non empty trivial 1 -element set
{{((- niltonil) + niltonil),(V,niltonil,(- 1r))},{((- niltonil) + niltonil)}} is set
the addF of V . [((- niltonil) + niltonil),(V,niltonil,(- 1r))] is set
(0. V) + (V,niltonil,(- 1r)) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(V,niltonil,(- 1r))) is right_complementable Element of the carrier of V
[(0. V),(V,niltonil,(- 1r))] is set
{(0. V),(V,niltonil,(- 1r))} is set
{(0. V)} is non empty trivial 1 -element set
{{(0. V),(V,niltonil,(- 1r))},{(0. V)}} is set
the addF of V . [(0. V),(V,niltonil,(- 1r))] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
niltonil is right_complementable Element of the carrier of V
- niltonil is right_complementable Element of the carrier of V
niltonil - (- niltonil) is right_complementable Element of the carrier of V
- (- niltonil) is right_complementable Element of the carrier of V
niltonil + (- (- niltonil)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,(- (- niltonil))) is right_complementable Element of the carrier of V
[niltonil,(- (- niltonil))] is set
{niltonil,(- (- niltonil))} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(- (- niltonil))},{niltonil}} is set
the addF of V . [niltonil,(- (- niltonil))] is set
niltonil + niltonil is right_complementable Element of the carrier of V
the addF of V . (niltonil,niltonil) is right_complementable Element of the carrier of V
[niltonil,niltonil] is set
{niltonil,niltonil} is set
{{niltonil,niltonil},{niltonil}} is set
the addF of V . [niltonil,niltonil] is set
(V,niltonil,1r) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[1r,niltonil] is set
{1r,niltonil} is set
{1r} is non empty trivial 1 -element set
{{1r,niltonil},{1r}} is set
the of V . [1r,niltonil] is set
(V,niltonil,1r) + niltonil is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,1r),niltonil) is right_complementable Element of the carrier of V
[(V,niltonil,1r),niltonil] is set
{(V,niltonil,1r),niltonil} is set
{(V,niltonil,1r)} is non empty trivial 1 -element set
{{(V,niltonil,1r),niltonil},{(V,niltonil,1r)}} is set
the addF of V . [(V,niltonil,1r),niltonil] is set
(V,niltonil,1r) + (V,niltonil,1r) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,1r),(V,niltonil,1r)) is right_complementable Element of the carrier of V
[(V,niltonil,1r),(V,niltonil,1r)] is set
{(V,niltonil,1r),(V,niltonil,1r)} is set
{{(V,niltonil,1r),(V,niltonil,1r)},{(V,niltonil,1r)}} is set
the addF of V . [(V,niltonil,1r),(V,niltonil,1r)] is set
1r + 1r is complex Element of COMPLEX
(V,niltonil,(1r + 1r)) is right_complementable Element of the carrier of V
[(1r + 1r),niltonil] is set
{(1r + 1r),niltonil} is set
{(1r + 1r)} is non empty trivial 1 -element set
{{(1r + 1r),niltonil},{(1r + 1r)}} is set
the of V . [(1r + 1r),niltonil] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
niltonil is right_complementable Element of the carrier of V
niltonil + niltonil 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,niltonil) is right_complementable Element of the carrier of V
[niltonil,niltonil] is set
{niltonil,niltonil} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,niltonil},{niltonil}} is set
the addF of V . [niltonil,niltonil] is set
- niltonil is right_complementable Element of the carrier of V
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
- niltonil is right_complementable Element of the carrier of V
X is complex set
(V,(- niltonil),X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,(- niltonil)] is set
{X,(- niltonil)} is set
{X} is non empty trivial 1 -element set
{{X,(- niltonil)},{X}} is set
the of V . [X,(- niltonil)] is set
- X is complex set
(V,niltonil,(- X)) is right_complementable Element of the carrier of V
[(- X),niltonil] is set
{(- X),niltonil} is set
{(- X)} is non empty trivial 1 -element set
{{(- X),niltonil},{(- X)}} is set
the of V . [(- X),niltonil] is set
(V,niltonil,(- 1r)) is right_complementable Element of the carrier of V
[(- 1r),niltonil] is set
{(- 1r),niltonil} is set
{(- 1r)} is non empty trivial 1 -element set
{{(- 1r),niltonil},{(- 1r)}} is set
the of V . [(- 1r),niltonil] is set
(V,(V,niltonil,(- 1r)),X) is right_complementable Element of the carrier of V
[X,(V,niltonil,(- 1r))] is set
{X,(V,niltonil,(- 1r))} is set
{{X,(V,niltonil,(- 1r))},{X}} is set
the of V . [X,(V,niltonil,(- 1r))] is set
X * (- 1r) is complex set
(V,niltonil,(X * (- 1r))) is right_complementable Element of the carrier of V
[(X * (- 1r)),niltonil] is set
{(X * (- 1r)),niltonil} is set
{(X * (- 1r))} is non empty trivial 1 -element set
{{(X * (- 1r)),niltonil},{(X * (- 1r))}} is set
the of V . [(X * (- 1r)),niltonil] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
- niltonil is right_complementable Element of the carrier of V
X is complex set
(V,(- niltonil),X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,(- niltonil)] is set
{X,(- niltonil)} is set
{X} is non empty trivial 1 -element set
{{X,(- niltonil)},{X}} is set
the of V . [X,(- niltonil)] is set
(V,niltonil,X) is right_complementable Element of the carrier of V
[X,niltonil] is set
{X,niltonil} is set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
- (V,niltonil,X) is right_complementable Element of the carrier of V
1r * X is complex set
- (1r * X) is complex set
(V,niltonil,(- (1r * X))) is right_complementable Element of the carrier of V
[(- (1r * X)),niltonil] is set
{(- (1r * X)),niltonil} is set
{(- (1r * X))} is non empty trivial 1 -element set
{{(- (1r * X)),niltonil},{(- (1r * X))}} is set
the of V . [(- (1r * X)),niltonil] is set
(- 1r) * X is complex set
(V,niltonil,((- 1r) * X)) is right_complementable Element of the carrier of V
[((- 1r) * X),niltonil] is set
{((- 1r) * X),niltonil} is set
{((- 1r) * X)} is non empty trivial 1 -element set
{{((- 1r) * X),niltonil},{((- 1r) * X)}} is set
the of V . [((- 1r) * X),niltonil] is set
(V,(V,niltonil,X),(- 1r)) is right_complementable Element of the carrier of V
[(- 1r),(V,niltonil,X)] is set
{(- 1r),(V,niltonil,X)} is set
{(- 1r)} is non empty trivial 1 -element set
{{(- 1r),(V,niltonil,X)},{(- 1r)}} is set
the of V . [(- 1r),(V,niltonil,X)] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
- niltonil is right_complementable Element of the carrier of V
X is complex set
- X is complex set
(V,(- niltonil),(- X)) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[(- X),(- niltonil)] is set
{(- X),(- niltonil)} is set
{(- X)} is non empty trivial 1 -element set
{{(- X),(- niltonil)},{(- X)}} is set
the of V . [(- X),(- niltonil)] is set
(V,niltonil,X) is right_complementable Element of the carrier of V
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
- (- X) is complex set
(V,niltonil,(- (- X))) is right_complementable Element of the carrier of V
[(- (- X)),niltonil] is set
{(- (- X)),niltonil} is set
{(- (- X))} is non empty trivial 1 -element set
{{(- (- X)),niltonil},{(- (- X))}} is set
the of V . [(- (- X)),niltonil] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
X is right_complementable Element of the carrier of V
niltonil - X is right_complementable Element of the carrier of V
- X is right_complementable Element of the carrier of V
niltonil + (- X) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (niltonil,(- X)) is right_complementable Element of the carrier of V
[niltonil,(- X)] is set
{niltonil,(- X)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(- X)},{niltonil}} is set
the addF of V . [niltonil,(- X)] is set
z is complex set
(V,(niltonil - X),z) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[z,(niltonil - X)] is set
{z,(niltonil - X)} is set
{z} is non empty trivial 1 -element set
{{z,(niltonil - X)},{z}} is set
the of V . [z,(niltonil - X)] is set
(V,niltonil,z) is right_complementable Element of the carrier of V
[z,niltonil] is set
{z,niltonil} is set
{{z,niltonil},{z}} is set
the of V . [z,niltonil] is set
(V,X,z) is right_complementable Element of the carrier of V
[z,X] is set
{z,X} is set
{{z,X},{z}} is set
the of V . [z,X] is set
(V,niltonil,z) - (V,X,z) is right_complementable Element of the carrier of V
- (V,X,z) is right_complementable Element of the carrier of V
(V,niltonil,z) + (- (V,X,z)) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,z),(- (V,X,z))) is right_complementable Element of the carrier of V
[(V,niltonil,z),(- (V,X,z))] is set
{(V,niltonil,z),(- (V,X,z))} is set
{(V,niltonil,z)} is non empty trivial 1 -element set
{{(V,niltonil,z),(- (V,X,z))},{(V,niltonil,z)}} is set
the addF of V . [(V,niltonil,z),(- (V,X,z))] is set
(V,(- X),z) is right_complementable Element of the carrier of V
[z,(- X)] is set
{z,(- X)} is set
{{z,(- X)},{z}} is set
the of V . [z,(- X)] is set
(V,niltonil,z) + (V,(- X),z) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,z),(V,(- X),z)) is right_complementable Element of the carrier of V
[(V,niltonil,z),(V,(- X),z)] is set
{(V,niltonil,z),(V,(- X),z)} is set
{{(V,niltonil,z),(V,(- X),z)},{(V,niltonil,z)}} is set
the addF of V . [(V,niltonil,z),(V,(- X),z)] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
X is complex set
(V,niltonil,X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
z is complex set
X - z is complex set
(V,niltonil,(X - z)) is right_complementable Element of the carrier of V
[(X - z),niltonil] is set
{(X - z),niltonil} is set
{(X - z)} is non empty trivial 1 -element set
{{(X - z),niltonil},{(X - z)}} is set
the of V . [(X - z),niltonil] is set
(V,niltonil,z) is right_complementable Element of the carrier of V
[z,niltonil] is set
{z,niltonil} is set
{z} is non empty trivial 1 -element set
{{z,niltonil},{z}} is set
the of V . [z,niltonil] is set
(V,niltonil,X) - (V,niltonil,z) is right_complementable Element of the carrier of V
- (V,niltonil,z) is right_complementable Element of the carrier of V
(V,niltonil,X) + (- (V,niltonil,z)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((V,niltonil,X),(- (V,niltonil,z))) is right_complementable Element of the carrier of V
[(V,niltonil,X),(- (V,niltonil,z))] is set
{(V,niltonil,X),(- (V,niltonil,z))} is set
{(V,niltonil,X)} is non empty trivial 1 -element set
{{(V,niltonil,X),(- (V,niltonil,z))},{(V,niltonil,X)}} is set
the addF of V . [(V,niltonil,X),(- (V,niltonil,z))] is set
- z is complex set
X + (- z) is complex set
(V,niltonil,(X + (- z))) is right_complementable Element of the carrier of V
[(X + (- z)),niltonil] is set
{(X + (- z)),niltonil} is set
{(X + (- z))} is non empty trivial 1 -element set
{{(X + (- z)),niltonil},{(X + (- z))}} is set
the of V . [(X + (- z)),niltonil] is set
(V,niltonil,(- z)) is right_complementable Element of the carrier of V
[(- z),niltonil] is set
{(- z),niltonil} is set
{(- z)} is non empty trivial 1 -element set
{{(- z),niltonil},{(- z)}} is set
the of V . [(- z),niltonil] is set
(V,niltonil,X) + (V,niltonil,(- z)) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,X),(V,niltonil,(- z))) is right_complementable Element of the carrier of V
[(V,niltonil,X),(V,niltonil,(- z))] is set
{(V,niltonil,X),(V,niltonil,(- z))} is set
{{(V,niltonil,X),(V,niltonil,(- z))},{(V,niltonil,X)}} is set
the addF of V . [(V,niltonil,X),(V,niltonil,(- z))] is set
- niltonil is right_complementable Element of the carrier of V
(V,(- niltonil),z) is right_complementable Element of the carrier of V
[z,(- niltonil)] is set
{z,(- niltonil)} is set
{{z,(- niltonil)},{z}} is set
the of V . [z,(- niltonil)] is set
(V,niltonil,X) + (V,(- niltonil),z) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,X),(V,(- niltonil),z)) is right_complementable Element of the carrier of V
[(V,niltonil,X),(V,(- niltonil),z)] is set
{(V,niltonil,X),(V,(- niltonil),z)} is set
{{(V,niltonil,X),(V,(- niltonil),z)},{(V,niltonil,X)}} is set
the addF of V . [(V,niltonil,X),(V,(- niltonil),z)] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is right_complementable Element of the carrier of V
X is right_complementable Element of the carrier of V
z is complex set
(V,niltonil,z) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[z,niltonil] is set
{z,niltonil} is set
{z} is non empty trivial 1 -element set
{{z,niltonil},{z}} is set
the of V . [z,niltonil] is set
(V,X,z) is right_complementable Element of the carrier of V
[z,X] is set
{z,X} is set
{{z,X},{z}} is set
the of V . [z,X] is set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
(V,niltonil,z) - (V,X,z) is right_complementable Element of the carrier of V
- (V,X,z) is right_complementable Element of the carrier of V
(V,niltonil,z) + (- (V,X,z)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((V,niltonil,z),(- (V,X,z))) is right_complementable Element of the carrier of V
[(V,niltonil,z),(- (V,X,z))] is set
{(V,niltonil,z),(- (V,X,z))} is set
{(V,niltonil,z)} is non empty trivial 1 -element set
{{(V,niltonil,z),(- (V,X,z))},{(V,niltonil,z)}} is set
the addF of V . [(V,niltonil,z),(- (V,X,z))] is set
niltonil - X is right_complementable Element of the carrier of V
- X is right_complementable Element of the carrier of V
niltonil + (- X) is right_complementable Element of the carrier of V
the addF of V . (niltonil,(- X)) is right_complementable Element of the carrier of V
[niltonil,(- X)] is set
{niltonil,(- X)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(- X)},{niltonil}} is set
the addF of V . [niltonil,(- X)] is set
(V,(niltonil - X),z) is right_complementable Element of the carrier of V
[z,(niltonil - X)] is set
{z,(niltonil - X)} is set
{{z,(niltonil - X)},{z}} is set
the of V . [z,(niltonil - X)] is set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
0. V is zero right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
niltonil is right_complementable Element of the carrier of V
X is complex set
(V,niltonil,X) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[X,niltonil] is set
{X,niltonil} is set
{X} is non empty trivial 1 -element set
{{X,niltonil},{X}} is set
the of V . [X,niltonil] is set
z is complex set
(V,niltonil,z) is right_complementable Element of the carrier of V
[z,niltonil] is set
{z,niltonil} is set
{z} is non empty trivial 1 -element set
{{z,niltonil},{z}} is set
the of V . [z,niltonil] is set
(V,niltonil,X) - (V,niltonil,z) is right_complementable Element of the carrier of V
- (V,niltonil,z) is right_complementable Element of the carrier of V
(V,niltonil,X) + (- (V,niltonil,z)) 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((V,niltonil,X),(- (V,niltonil,z))) is right_complementable Element of the carrier of V
[(V,niltonil,X),(- (V,niltonil,z))] is set
{(V,niltonil,X),(- (V,niltonil,z))} is set
{(V,niltonil,X)} is non empty trivial 1 -element set
{{(V,niltonil,X),(- (V,niltonil,z))},{(V,niltonil,X)}} is set
the addF of V . [(V,niltonil,X),(- (V,niltonil,z))] is set
X - z is complex set
(V,niltonil,(X - z)) is right_complementable Element of the carrier of V
[(X - z),niltonil] is set
{(X - z),niltonil} is set
{(X - z)} is non empty trivial 1 -element set
{{(X - z),niltonil},{(X - z)}} is set
the of V . [(X - z),niltonil] is set
- z is complex set
(- z) + X is complex set
V is non empty addLoopStr
the carrier of V is non empty set
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V50() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of V
[:NAT, the carrier of V:] is non empty V50() set
Sum (<*> the carrier of V) is Element of the carrier of V
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
bool [:NAT, the carrier of V:] is non empty V50() set
len (<*> the carrier of V) is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V50() cardinal {} -element FinSequence-membered Element of NAT
X 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:]
X . (len (<*> the carrier of V)) is Element of the carrier of V
X . 0 is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
niltonil is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len niltonil is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
Sum niltonil is Element of the carrier of V
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V50() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of V
[:NAT, the carrier of V:] is non empty V50() set
V is non empty right_complementable Abelian add-associative right_zeroed () () () () ()
the carrier of V is non empty set
niltonil is complex set
X is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len X is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
z is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len z is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
dom X is Element of bool NAT
Sum X is right_complementable Element of the carrier of V
Sum z is right_complementable Element of the carrier of V
(V,(Sum z),niltonil) is right_complementable Element of the carrier of V
the of V is Relation-like [:COMPLEX, the carrier of V:] -defined the carrier of V -valued Function-like V18([:COMPLEX, the carrier of V:], the carrier of V) Element of bool [:[:COMPLEX, the carrier of V:], the carrier of V:]
[:COMPLEX, the carrier of V:] is non empty V50() set
[:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
bool [:[:COMPLEX, the carrier of V:], the carrier of V:] is non empty V50() set
[niltonil,(Sum z)] is set
{niltonil,(Sum z)} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(Sum z)},{niltonil}} is set
the of V . [niltonil,(Sum z)] is set
Seg (len X) is V50() len X -element Element of bool NAT
CNS is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
S is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
g is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len g is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
CNS + 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
Seg (len S) is V50() len S -element Element of bool NAT
Seg CNS is V50() CNS -element Element of bool NAT
S | (Seg CNS) is Relation-like NAT -defined the carrier of V -valued Function-like FinSubsequence-like Element of bool [:NAT, the carrier of V:]
[:NAT, the carrier of V:] is non empty V50() set
bool [:NAT, the carrier of V:] is non empty V50() set
g | (Seg CNS) is Relation-like NAT -defined the carrier of V -valued Function-like FinSubsequence-like Element of bool [:NAT, the carrier of V:]
r is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len r is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
h is Relation-like NAT -defined the carrier of V -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len h is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
Seg (len h) is V50() len h -element Element of bool NAT
dom h is Element of bool NAT
m1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real V50() cardinal Element of NAT
k is right_complementable Element of the carrier of V
r . m1 is set
dom r is Element of bool NAT
g . m1 is set
S . m1 is set
(V,k,niltonil) is right_complementable Element of the carrier of V
[niltonil,k] is set
{niltonil,k} is set
{{niltonil,k},{niltonil}} is set
the of V . [niltonil,k] is set
h . m1 is set
Seg (CNS + 1) is V50() CNS + 1 -element Element of bool NAT
dom S is Element of bool NAT
dom g is Element of bool NAT
S . (CNS + 1) is set
g . (CNS + 1) is set
m1 is right_complementable Element of the carrier of V
k is right_complementable Element of the carrier of V
(V,k,niltonil) is right_complementable Element of the carrier of V
[niltonil,k] is set
{niltonil,k} is set
{{niltonil,k},{niltonil}} is set
the of V . [niltonil,k] is set
Seg (len r) is V50() len r -element Element of bool NAT
Sum S is right_complementable Element of the carrier of V
Sum h is right_complementable Element of the carrier of V
(Sum h)