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