:: CLVECT_1 semantic presentation

REAL is non empty V50() set

bool REAL is non empty V50() set
COMPLEX is non empty V50() set

bool omega is non empty V50() set
bool NAT is non empty V50() set
is non empty V50() set
bool is non empty V50() set
{} is set

{{},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

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,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
is non empty V50() set
[:,V:] is non empty V50() set
bool [:,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:]

(V,niltonil,X,z) is () ()

op2 is Relation-like [:1,1:] -defined 1 -valued Function-like V18([:1,1:],1) Element of bool [:[:1,1:],1:]

is non empty V50() set
[:,1:] is non empty V50() set
bool [:,1:] is non empty V50() set
(1,op0,op2,(pr2 (COMPLEX,1))) is non empty () ()
() is () ()
the carrier of () is set
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
is non empty trivial 1 -element set
{{1r,niltonil},} 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

(V,niltonil,0c) is right_complementable Element of the carrier of V
[0c,niltonil] is set
{0c,niltonil} is set
is non empty trivial 1 -element set
{{0c,niltonil},} 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
is non empty trivial 1 -element set
{{1r,niltonil},} 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

(V,niltonil,()) is right_complementable Element of the carrier of V
[(),niltonil] is set
{(),niltonil} is set
{()} is non empty trivial 1 -element set
{{(),niltonil},{()}} is set
the of V . [(),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

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
is non empty trivial 1 -element set
{{1r,niltonil},} 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

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,()) 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] is set
{(),niltonil} is set
{()} is non empty trivial 1 -element set
{{(),niltonil},{()}} is set
the of V . [(),niltonil] is set
niltonil + (V,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,(V,niltonil,())) is right_complementable Element of the carrier of V
[niltonil,(V,niltonil,())] is set
{niltonil,(V,niltonil,())} is set
{niltonil} is non empty trivial 1 -element set
{{niltonil,(V,niltonil,())},{niltonil}} is set
the addF of V . [niltonil,(V,niltonil,())] is set
(V,niltonil,1r) is right_complementable Element of the carrier of V
[1r,niltonil] is set
{1r,niltonil} is set
is non empty trivial 1 -element set
{{1r,niltonil},} is set
the of V . [1r,niltonil] is set
(V,niltonil,1r) + (V,niltonil,()) is right_complementable Element of the carrier of V
the addF of V . ((V,niltonil,1r),(V,niltonil,())) is right_complementable Element of the carrier of V
[(V,niltonil,1r),(V,niltonil,())] is set
{(V,niltonil,1r),(V,niltonil,())} is set
{(V,niltonil,1r)} is non empty trivial 1 -element set
{{(V,niltonil,1r),(V,niltonil,())},{(V,niltonil,1r)}} is set
the addF of V . [(V,niltonil,1r),(V,niltonil,())] is set
1r + () is complex Element of COMPLEX
(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
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,())) is right_complementable Element of the carrier of V
the addF of V . ((- niltonil),(niltonil + (V,niltonil,()))) is right_complementable Element of the carrier of V
[(- niltonil),(niltonil + (V,niltonil,()))] is set
{(- niltonil),(niltonil + (V,niltonil,()))} is set
{(- niltonil)} is non empty trivial 1 -element set
{{(- niltonil),(niltonil + (V,niltonil,()))},{(- niltonil)}} is set
the addF of V . [(- niltonil),(niltonil + (V,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
((- niltonil) + niltonil) + (V,niltonil,()) is right_complementable Element of the carrier of V
the addF of V . (((- niltonil) + niltonil),(V,niltonil,())) is right_complementable Element of the carrier of V
[((- niltonil) + niltonil),(V,niltonil,())] is set
{((- niltonil) + niltonil),(V,niltonil,())} is set
{((- niltonil) + niltonil)} is non empty trivial 1 -element set
{{((- niltonil) + niltonil),(V,niltonil,())},{((- niltonil) + niltonil)}} is set
the addF of V . [((- niltonil) + niltonil),(V,niltonil,())] is set
(0. V) + (V,niltonil,()) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(V,niltonil,())) is right_complementable Element of the carrier of V
[(0. V),(V,niltonil,())] is set
{(0. V),(V,niltonil,())} is set
{(0. V)} is non empty trivial 1 -element set
{{(0. V),(V,niltonil,())},{(0. V)}} is set
the addF of V . [(0. V),(V,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 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
is non empty trivial 1 -element set
{{1r,niltonil},} 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

(V,niltonil,()) is right_complementable Element of the carrier of V
[(),niltonil] is set
{(),niltonil} is set
{()} is non empty trivial 1 -element set
{{(),niltonil},{()}} is set
the of V . [(),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,()) is right_complementable Element of the carrier of V
[(),niltonil] is set
{(),niltonil} is set
{()} is non empty trivial 1 -element set
{{(),niltonil},{()}} is set
the of V . [(),niltonil] is set
(V,(V,niltonil,()),X) is right_complementable Element of the carrier of V
[X,(V,niltonil,())] is set
{X,(V,niltonil,())} is set
{{X,(V,niltonil,())},{X}} is set
the of V . [X,(V,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
- 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
(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
() * 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,(V,niltonil,X),()) is right_complementable Element of the carrier of V
[(),(V,niltonil,X)] is set
{(),(V,niltonil,X)} is set
{()} is non empty trivial 1 -element set
{{(),(V,niltonil,X)},{()}} is set
the of V . [(),(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

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

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

Sum niltonil is Element 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

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

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

Seg (len h) is V50() len h -element Element of bool NAT
dom h is Element of bool 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)