REAL is non empty V33() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V33() countable denumerable Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V33() set
omega is non empty epsilon-transitive epsilon-connected ordinal V33() countable denumerable set
bool omega is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty Relation-like set
bool [:NAT,REAL:] is non empty set
K190() is non empty set
[:K190(),K190():] is non empty Relation-like set
[:[:K190(),K190():],K190():] is non empty Relation-like set
bool [:[:K190(),K190():],K190():] is non empty set
[:REAL,K190():] is non empty Relation-like set
[:[:REAL,K190():],K190():] is non empty Relation-like set
bool [:[:REAL,K190():],K190():] is non empty set
K196() is RLSStruct
the carrier of K196() is set
bool the carrier of K196() is non empty set
K200() is Element of bool the carrier of K196()
[:K200(),K200():] is Relation-like set
[:[:K200(),K200():],REAL:] is Relation-like set
bool [:[:K200(),K200():],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of K196()
[:the_set_of_l1RealSequences,REAL:] is Relation-like set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
RAT is non empty V33() set
INT is non empty V33() set
[:REAL,REAL:] is non empty Relation-like set
bool [:REAL,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty Relation-like set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty Relation-like set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty Relation-like set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty Relation-like set
[:[:NAT,NAT:],NAT:] is non empty Relation-like set
bool [:[:NAT,NAT:],NAT:] is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty Relation-like set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
[:2,2:] is non empty Relation-like set
[:[:2,2:],REAL:] is non empty Relation-like set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() TopSpace-like V198() L20()
the carrier of (TOP-REAL 2) is non empty set
K646() is TopStruct
the carrier of K646() is set
K506() is V182() L19()
K651() is TopSpace-like TopStruct
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V140() V141() V142() Cardinal-yielding countable set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
- 1 is V11() real ext-real Element of REAL
Seg 1 is non empty V33() V40(1) countable Element of bool NAT
{1} is non empty set
Seg 2 is non empty V33() V40(2) countable Element of bool NAT
{1,2} is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V140() V141() V142() Cardinal-yielding countable Element of NAT
X is non empty set
Y is non empty set
[:X,Y:] is non empty Relation-like set
I is non empty set
J is non empty set
[:I,J:] is non empty Relation-like set
[:[:X,Y:],[:I,J:]:] is non empty Relation-like set
[:X,I:] is non empty Relation-like set
[:Y,J:] is non empty Relation-like set
[:[:X,I:],[:Y,J:]:] is non empty Relation-like set
[:[:[:X,Y:],[:I,J:]:],[:[:X,I:],[:Y,J:]:]:] is non empty Relation-like set
bool [:[:[:X,Y:],[:I,J:]:],[:[:X,I:],[:Y,J:]:]:] is non empty set
K is set
K is set
v is set
r is set
[v,r] is set
yy is set
x1 is set
[yy,x1] is set
[v,yy] is set
[r,x1] is set
[[v,yy],[r,x1]] is set
K is non empty Relation-like [:[:X,Y:],[:I,J:]:] -defined [:[:X,I:],[:Y,J:]:] -valued Function-like V26([:[:X,Y:],[:I,J:]:]) quasi_total Element of bool [:[:[:X,Y:],[:I,J:]:],[:[:X,I:],[:Y,J:]:]:]
K is set
v is set
r is set
yy is set
[K,v] is set
[r,yy] is set
K . ([K,v],[r,yy]) is set
[[K,v],[r,yy]] is set
K . [[K,v],[r,yy]] is set
[K,r] is set
[v,yy] is set
[[K,r],[v,yy]] is set
x1 is set
y1 is set
xx2 is set
yy2 is set
[x1,y1] is set
[xx2,yy2] is set
[x1,xx2] is set
[y1,yy2] is set
[[x1,xx2],[y1,yy2]] is set
K is set
v is set
K . K is set
K . v is set
r is set
yy is set
[r,yy] is set
x1 is set
y1 is set
[x1,y1] is set
xx2 is set
yy2 is set
[xx2,yy2] is set
I is set
v is set
[I,v] is set
x1 is set
y1 is set
[x1,y1] is set
v1 is set
Ix1 is set
[v1,Ix1] is set
[x1,xx2] is set
[y1,yy2] is set
[[x1,xx2],[y1,yy2]] is set
K . ([x1,y1],[xx2,yy2]) is set
[[x1,y1],[xx2,yy2]] is set
K . [[x1,y1],[xx2,yy2]] is set
K . ([x1,y1],[v1,Ix1]) is set
[[x1,y1],[v1,Ix1]] is set
K . [[x1,y1],[v1,Ix1]] is set
[x1,v1] is set
[y1,Ix1] is set
[[x1,v1],[y1,Ix1]] is set
K is set
v is set
r is set
[v,r] is set
yy is set
x1 is set
[yy,x1] is set
y1 is set
xx2 is set
[y1,xx2] is set
[yy,y1] is set
[x1,xx2] is set
[[yy,y1],[x1,xx2]] is set
K . ([yy,y1],[x1,xx2]) is set
K . [[yy,y1],[x1,xx2]] is set
yy2 is Element of [:[:X,Y:],[:I,J:]:]
K . yy2 is Element of [:[:X,I:],[:Y,J:]:]
rng K is non empty Relation-like [:X,I:] -defined [:Y,J:] -valued Element of bool [:[:X,I:],[:Y,J:]:]
bool [:[:X,I:],[:Y,J:]:] is non empty set
{1} is non empty countable Element of bool NAT
X is non empty set
Y is Relation-like Function-like set
dom Y is set
Y . 1 is set
product Y is functional with_common_domain product-like set
[:X,(product Y):] is Relation-like set
bool [:X,(product Y):] is non empty set
I is set
<*I*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like countable set
dom <*I*> is non empty countable Element of bool NAT
len <*I*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len <*I*>) is V33() V40( len <*I*>) countable Element of bool NAT
J is set
<*I*> . J is set
Y . J is set
I is Relation-like X -defined product Y -valued Function-like quasi_total Element of bool [:X,(product Y):]
rng Y is set
J is set
Y . J is set
J is set
K is set
I . J is Relation-like Function-like set
I . K is Relation-like Function-like set
<*J*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like countable set
<*K*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like countable set
J is set
K is Relation-like Function-like set
dom K is set
K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K . 1 is set
len K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
<*(K . 1)*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like countable set
I . (K . 1) is Relation-like Function-like set
rng I is functional with_common_domain Element of bool (product Y)
bool (product Y) is non empty set
{1,2} is non empty countable Element of bool NAT
X is non empty set
Y is non empty set
[:X,Y:] is non empty Relation-like set
I is Relation-like Function-like set
dom I is set
I . 1 is set
I . 2 is set
product I is functional with_common_domain product-like set
[:[:X,Y:],(product I):] is Relation-like set
bool [:[:X,Y:],(product I):] is non empty set
J is set
K is set
<*J,K*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like countable set
dom <*J,K*> is non empty countable Element of bool NAT
len <*J,K*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len <*J,K*>) is V33() V40( len <*J,K*>) countable Element of bool NAT
K is set
<*J,K*> . K is set
I . K is set
J is Relation-like [:X,Y:] -defined product I -valued Function-like quasi_total Element of bool [:[:X,Y:],(product I):]
rng I is set
K is set
I . K is set
K is set
K is set
J . K is Relation-like Function-like set
J . K is Relation-like Function-like set
v is set
r is set
[v,r] is set
yy is set
x1 is set
[yy,x1] is set
<*v,r*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like countable set
J . (v,r) is set
J . [v,r] is Relation-like Function-like set
J . (yy,x1) is set
J . [yy,x1] is Relation-like Function-like set
<*yy,x1*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like countable set
K is set
K is Relation-like Function-like set
dom K is set
v is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
v . 1 is set
v . 2 is set
len v is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
<*(v . 1),(v . 2)*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like countable set
[(v . 1),(v . 2)] is set
J . ((v . 1),(v . 2)) is set
J . [(v . 1),(v . 2)] is Relation-like Function-like set
x1 is Element of [:X,Y:]
J . x1 is Relation-like Function-like Element of product I
rng J is functional with_common_domain Element of bool (product I)
bool (product I) is non empty set
X is non empty set
<*X*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like countable set
product <*X*> is functional with_common_domain product-like set
[:X,(product <*X*>):] is Relation-like set
bool [:X,(product <*X*>):] is non empty set
dom <*X*> is non empty countable Element of bool NAT
<*X*> . 1 is set
X is non empty Relation-like non-empty NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
Y is non empty Relation-like non-empty NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
X ^ Y is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
I is set
dom (X ^ Y) is non empty countable Element of bool NAT
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
dom X is non empty countable Element of bool NAT
X . J is set
(X ^ Y) . J is set
(X ^ Y) . I is set
dom Y is non empty countable Element of bool NAT
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
len X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(len X) + K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(len X) + K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Y . K is set
(X ^ Y) . J is set
(X ^ Y) . I is set
J is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
dom X is non empty countable Element of bool NAT
dom Y is non empty countable Element of bool NAT
len X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
X is non empty set
Y is non empty set
[:X,Y:] is non empty Relation-like set
<*X,Y*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like countable set
product <*X,Y*> is functional with_common_domain product-like set
[:[:X,Y:],(product <*X,Y*>):] is Relation-like set
bool [:[:X,Y:],(product <*X,Y*>):] is non empty set
dom <*X,Y*> is non empty countable Element of bool NAT
<*X,Y*> . 1 is set
<*X,Y*> . 2 is set
X is non empty Relation-like non-empty NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
product X is non empty functional with_common_domain product-like set
Y is non empty Relation-like non-empty NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
product Y is non empty functional with_common_domain product-like set
[:(product X),(product Y):] is non empty Relation-like set
X ^ Y is non empty Relation-like non-empty NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
product (X ^ Y) is non empty functional with_common_domain product-like set
[:[:(product X),(product Y):],(product (X ^ Y)):] is non empty Relation-like set
bool [:[:(product X),(product Y):],(product (X ^ Y)):] is non empty set
I is set
J is set
dom X is non empty countable Element of bool NAT
K is Relation-like Function-like set
dom K is set
len X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len X) is V33() V40( len X) countable Element of bool NAT
dom Y is non empty countable Element of bool NAT
v is Relation-like Function-like set
dom v is set
len Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len Y) is V33() V40( len Y) countable Element of bool NAT
K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
len K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
len r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K ^ r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
dom (K ^ r) is countable Element of bool NAT
(len K) + (len r) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg ((len K) + (len r)) is V33() V40((len K) + (len r)) countable Element of bool NAT
len (X ^ Y) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len (X ^ Y)) is V33() V40( len (X ^ Y)) countable Element of bool NAT
dom (X ^ Y) is non empty countable Element of bool NAT
yy is set
(K ^ r) . yy is set
(X ^ Y) . yy is set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K . x1 is set
X . x1 is set
(K ^ r) . x1 is set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(len X) + y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
(len X) + y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
r . y1 is set
Y . y1 is set
(K ^ r) . x1 is set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
I is non empty Relation-like [:(product X),(product Y):] -defined product (X ^ Y) -valued Function-like V26([:(product X),(product Y):]) quasi_total Element of bool [:[:(product X),(product Y):],(product (X ^ Y)):]
J is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
I . (J,K) is set
[J,K] is set
I . [J,K] is Relation-like Function-like set
J ^ K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
v is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K ^ v is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
J is set
K is set
I . J is Relation-like Function-like set
I . K is Relation-like Function-like set
K is set
v is set
[K,v] is set
r is set
yy is set
[r,yy] is set
I . (K,v) is set
I . [K,v] is Relation-like Function-like set
x1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
y1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
x1 ^ y1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
I . (r,yy) is set
I . [r,yy] is Relation-like Function-like set
xx2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
yy2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
xx2 ^ yy2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
dom x1 is countable Element of bool NAT
dom X is non empty countable Element of bool NAT
dom xx2 is countable Element of bool NAT
(x1 ^ y1) | (dom x1) is Relation-like NAT -defined dom x1 -defined NAT -defined Function-like FinSubsequence-like set
J is set
dom (X ^ Y) is non empty countable Element of bool NAT
K is Relation-like Function-like set
dom K is set
len (X ^ Y) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
Seg (len (X ^ Y)) is V33() V40( len (X ^ Y)) countable Element of bool NAT
len X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K | (len X) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
K /^ (len X) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
rng K is set
(K | (len X)) ^ (K /^ (len X)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
len Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
(len X) + (len Y) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
len K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
len (K | (len X)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
dom (K | (len X)) is countable Element of bool NAT
Seg (len X) is V33() V40( len X) countable Element of bool NAT
yy is set
(K | (len X)) . yy is set
X . yy is set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
(K | (len X)) . x1 is set
K . x1 is set
X . x1 is set
(X ^ Y) . x1 is set
len (K /^ (len X)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
(len K) - (len X) is V11() real ext-real Element of REAL
Seg (len (K /^ (len X))) is V33() V40( len (K /^ (len X))) countable Element of bool NAT
dom Y is non empty countable Element of bool NAT
dom (K /^ (len X)) is countable Element of bool NAT
yy is set
(K /^ (len X)) . yy is set
Y . yy is set
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
(K /^ (len X)) . x1 is set
(len X) + x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real Element of NAT
K . ((len X) + x1) is set
Y . x1 is set
(X ^ Y) . ((len X) + x1) is set
[(K | (len X)),(K /^ (len X))] is set
I . ((K | (len X)),(K /^ (len X))) is set
I . [(K | (len X)),(K /^ (len X))] is Relation-like Function-like set
yy is Element of [:(product X),(product Y):]
I . yy is Relation-like NAT -defined Function-like X ^ Y -compatible Element of product (X ^ Y)
rng I is non empty functional with_common_domain Element of bool (product (X ^ Y))
bool (product (X ^ Y)) is non empty set
I is set
X is non empty 1-sorted
the carrier of X is non empty set
Y is non empty 1-sorted
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
X is non empty addLoopStr
the carrier of X is non empty set
Y is non empty addLoopStr
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
I is set
J is set
K is Element of the carrier of X
K is Element of the carrier of Y
[K,K] is Element of [: the carrier of X, the carrier of Y:]
v is Element of the carrier of X
r is Element of the carrier of Y
[v,r] is Element of [: the carrier of X, the carrier of Y:]
K + v is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (K,v) is Element of the carrier of X
[K,v] is set
the addF of X . [K,v] is set
K + r is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (K,r) is Element of the carrier of Y
[K,r] is set
the addF of Y . [K,r] is set
[(K + v),(K + r)] is Element of [: the carrier of X, the carrier of Y:]
yy is Element of [: the carrier of X, the carrier of Y:]
x1 is Element of the carrier of X
xx2 is Element of the carrier of Y
[x1,xx2] is Element of [: the carrier of X, the carrier of Y:]
y1 is Element of the carrier of X
yy2 is Element of the carrier of Y
[y1,yy2] is Element of [: the carrier of X, the carrier of Y:]
x1 + y1 is Element of the carrier of X
the addF of X . (x1,y1) is Element of the carrier of X
[x1,y1] is set
the addF of X . [x1,y1] is set
xx2 + yy2 is Element of the carrier of Y
the addF of Y . (xx2,yy2) is Element of the carrier of Y
[xx2,yy2] is set
the addF of Y . [xx2,yy2] is set
[(x1 + y1),(xx2 + yy2)] is Element of [: the carrier of X, the carrier of Y:]
I is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
J is Element of the carrier of X
K is Element of the carrier of Y
[J,K] is Element of [: the carrier of X, the carrier of Y:]
K is Element of the carrier of X
v is Element of the carrier of Y
[K,v] is Element of [: the carrier of X, the carrier of Y:]
I . ([J,K],[K,v]) is Element of [: the carrier of X, the carrier of Y:]
[[J,K],[K,v]] is set
I . [[J,K],[K,v]] is set
r is Element of the carrier of X
x1 is Element of the carrier of Y
[r,x1] is Element of [: the carrier of X, the carrier of Y:]
yy is Element of the carrier of X
y1 is Element of the carrier of Y
[yy,y1] is Element of [: the carrier of X, the carrier of Y:]
r + yy is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (r,yy) is Element of the carrier of X
[r,yy] is set
the addF of X . [r,yy] is set
x1 + y1 is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (x1,y1) is Element of the carrier of Y
[x1,y1] is set
the addF of Y . [x1,y1] is set
[(r + yy),(x1 + y1)] is Element of [: the carrier of X, the carrier of Y:]
J + K is Element of the carrier of X
the addF of X . (J,K) is Element of the carrier of X
[J,K] is set
the addF of X . [J,K] is set
K + v is Element of the carrier of Y
the addF of Y . (K,v) is Element of the carrier of Y
[K,v] is set
the addF of Y . [K,v] is set
[(J + K),(K + v)] is Element of [: the carrier of X, the carrier of Y:]
I is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
J is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
K is Element of [: the carrier of X, the carrier of Y:]
v is Element of the carrier of X
r is Element of the carrier of Y
[v,r] is Element of [: the carrier of X, the carrier of Y:]
K is Element of [: the carrier of X, the carrier of Y:]
yy is Element of the carrier of X
x1 is Element of the carrier of Y
[yy,x1] is Element of [: the carrier of X, the carrier of Y:]
I . (K,K) is Element of [: the carrier of X, the carrier of Y:]
[K,K] is set
I . [K,K] is set
v + yy is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (v,yy) is Element of the carrier of X
[v,yy] is set
the addF of X . [v,yy] is set
r + x1 is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (r,x1) is Element of the carrier of Y
[r,x1] is set
the addF of Y . [r,x1] is set
[(v + yy),(r + x1)] is Element of [: the carrier of X, the carrier of Y:]
J . (K,K) is Element of [: the carrier of X, the carrier of Y:]
J . [K,K] is set
X is non empty RLSStruct
the carrier of X is non empty set
Y is non empty RLSStruct
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
[:REAL,[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
K is set
K is set
r is Element of the carrier of X
yy is Element of the carrier of Y
[r,yy] is Element of [: the carrier of X, the carrier of Y:]
v is V11() real ext-real Element of REAL
v * r is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty Relation-like set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
the Mult of X . (v,r) is set
[v,r] is set
the Mult of X . [v,r] is set
v * yy is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (v,yy) is set
[v,yy] is set
the Mult of Y . [v,yy] is set
[(v * r),(v * yy)] is Element of [: the carrier of X, the carrier of Y:]
y1 is V11() real ext-real Element of REAL
xx2 is Element of the carrier of X
yy2 is Element of the carrier of Y
[xx2,yy2] is Element of [: the carrier of X, the carrier of Y:]
y1 * xx2 is Element of the carrier of X
the Mult of X . (y1,xx2) is set
[y1,xx2] is set
the Mult of X . [y1,xx2] is set
y1 * yy2 is Element of the carrier of Y
the Mult of Y . (y1,yy2) is set
[y1,yy2] is set
the Mult of Y . [y1,yy2] is set
[(y1 * xx2),(y1 * yy2)] is Element of [: the carrier of X, the carrier of Y:]
K is non empty Relation-like [:REAL,[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:REAL,[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
K is V11() real ext-real Element of REAL
v is Element of the carrier of X
r is Element of the carrier of Y
[v,r] is Element of [: the carrier of X, the carrier of Y:]
K . (K,[v,r]) is Element of [: the carrier of X, the carrier of Y:]
[K,[v,r]] is set
K . [K,[v,r]] is set
yy is V11() real ext-real Element of REAL
x1 is Element of the carrier of X
y1 is Element of the carrier of Y
[x1,y1] is Element of [: the carrier of X, the carrier of Y:]
yy * x1 is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty Relation-like set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
the Mult of X . (yy,x1) is set
[yy,x1] is set
the Mult of X . [yy,x1] is set
yy * y1 is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (yy,y1) is set
[yy,y1] is set
the Mult of Y . [yy,y1] is set
[(yy * x1),(yy * y1)] is Element of [: the carrier of X, the carrier of Y:]
yy is V11() real ext-real Element of REAL
x1 is Element of the carrier of X
y1 is Element of the carrier of Y
[x1,y1] is Element of [: the carrier of X, the carrier of Y:]
yy * x1 is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty Relation-like set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
the Mult of X . (yy,x1) is set
[yy,x1] is set
the Mult of X . [yy,x1] is set
K * y1 is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (K,y1) is set
[K,y1] is set
the Mult of Y . [K,y1] is set
[(yy * x1),(K * y1)] is Element of [: the carrier of X, the carrier of Y:]
K * v is Element of the carrier of X
the Mult of X . (K,v) is set
[K,v] is set
the Mult of X . [K,v] is set
K * r is Element of the carrier of Y
the Mult of Y . (K,r) is set
[K,r] is set
the Mult of Y . [K,r] is set
[(K * v),(K * r)] is Element of [: the carrier of X, the carrier of Y:]
I is non empty Relation-like [:REAL,[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:REAL,[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
J is non empty Relation-like [:REAL,[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:REAL,[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
K is Element of [: the carrier of X, the carrier of Y:]
v is Element of the carrier of X
r is Element of the carrier of Y
[v,r] is Element of [: the carrier of X, the carrier of Y:]
K is V11() real ext-real Element of REAL
I . (K,K) is Element of [: the carrier of X, the carrier of Y:]
[K,K] is set
I . [K,K] is set
K * v is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty Relation-like set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
the Mult of X . (K,v) is set
[K,v] is set
the Mult of X . [K,v] is set
K * r is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty Relation-like set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (K,r) is set
[K,r] is set
the Mult of Y . [K,r] is set
[(K * v),(K * r)] is Element of [: the carrier of X, the carrier of Y:]
J . (K,K) is Element of [: the carrier of X, the carrier of Y:]
J . [K,K] is set
X is non empty addLoopStr
the carrier of X is non empty set
Y is non empty addLoopStr
the carrier of Y is non empty set
0. X is V52(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. Y is V52(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
X is non empty addLoopStr
the carrier of X is non empty set
Y is non empty addLoopStr
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
(X,Y) is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
(X,Y) is Element of [: the carrier of X, the carrier of Y:]
0. X is V52(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. Y is V52(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
addLoopStr(# [: the carrier of X, the carrier of Y:],(X,Y),(X,Y) #) is non empty strict addLoopStr
X is non empty Abelian addLoopStr
Y is non empty Abelian addLoopStr
(X,Y) is non empty strict addLoopStr
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
(X,Y) is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
(X,Y) is Element of [: the carrier of X, the carrier of Y:]
0. X is V52(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. Y is V52(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
addLoopStr(# [: the carrier of X, the carrier of Y:],(X,Y),(X,Y) #) is non empty strict addLoopStr
the carrier of (X,Y) is non empty set
I is Element of the carrier of (X,Y)
J is Element of the carrier of (X,Y)
I + J is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V26([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
the addF of (X,Y) . (I,J) is Element of the carrier of (X,Y)
[I,J] is set
the addF of (X,Y) . [I,J] is set
J + I is Element of the carrier of (X,Y)
the addF of (X,Y) . (J,I) is Element of the carrier of (X,Y)
[J,I] is set
the addF of (X,Y) . [J,I] is set
K is Element of the carrier of X
K is Element of the carrier of Y
[K,K] is Element of [: the carrier of X, the carrier of Y:]
v is Element of the carrier of X
r is Element of the carrier of Y
[v,r] is Element of [: the carrier of X, the carrier of Y:]
K + v is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (K,v) is Element of the carrier of X
[K,v] is set
the addF of X . [K,v] is set
K + r is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (K,r) is Element of the carrier of Y
[K,r] is set
the addF of Y . [K,r] is set
[(K + v),(K + r)] is Element of [: the carrier of X, the carrier of Y:]
X is non empty add-associative addLoopStr
Y is non empty add-associative addLoopStr
(X,Y) is non empty strict addLoopStr
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
(X,Y) is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
(X,Y) is Element of [: the carrier of X, the carrier of Y:]
0. X is V52(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. Y is V52(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
addLoopStr(# [: the carrier of X, the carrier of Y:],(X,Y),(X,Y) #) is non empty strict addLoopStr
the carrier of (X,Y) is non empty set
I is Element of the carrier of (X,Y)
J is Element of the carrier of (X,Y)
I + J is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V26([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
the addF of (X,Y) . (I,J) is Element of the carrier of (X,Y)
[I,J] is set
the addF of (X,Y) . [I,J] is set
K is Element of the carrier of (X,Y)
(I + J) + K is Element of the carrier of (X,Y)
the addF of (X,Y) . ((I + J),K) is Element of the carrier of (X,Y)
[(I + J),K] is set
the addF of (X,Y) . [(I + J),K] is set
J + K is Element of the carrier of (X,Y)
the addF of (X,Y) . (J,K) is Element of the carrier of (X,Y)
[J,K] is set
the addF of (X,Y) . [J,K] is set
I + (J + K) is Element of the carrier of (X,Y)
the addF of (X,Y) . (I,(J + K)) is Element of the carrier of (X,Y)
[I,(J + K)] is set
the addF of (X,Y) . [I,(J + K)] is set
K is Element of the carrier of X
v is Element of the carrier of Y
[K,v] is Element of [: the carrier of X, the carrier of Y:]
r is Element of the carrier of X
yy is Element of the carrier of Y
[r,yy] is Element of [: the carrier of X, the carrier of Y:]
x1 is Element of the carrier of X
y1 is Element of the carrier of Y
[x1,y1] is Element of [: the carrier of X, the carrier of Y:]
K + r is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (K,r) is Element of the carrier of X
[K,r] is set
the addF of X . [K,r] is set
(K + r) + x1 is Element of the carrier of X
the addF of X . ((K + r),x1) is Element of the carrier of X
[(K + r),x1] is set
the addF of X . [(K + r),x1] is set
r + x1 is Element of the carrier of X
the addF of X . (r,x1) is Element of the carrier of X
[r,x1] is set
the addF of X . [r,x1] is set
K + (r + x1) is Element of the carrier of X
the addF of X . (K,(r + x1)) is Element of the carrier of X
[K,(r + x1)] is set
the addF of X . [K,(r + x1)] is set
v + yy is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (v,yy) is Element of the carrier of Y
[v,yy] is set
the addF of Y . [v,yy] is set
(v + yy) + y1 is Element of the carrier of Y
the addF of Y . ((v + yy),y1) is Element of the carrier of Y
[(v + yy),y1] is set
the addF of Y . [(v + yy),y1] is set
yy + y1 is Element of the carrier of Y
the addF of Y . (yy,y1) is Element of the carrier of Y
[yy,y1] is set
the addF of Y . [yy,y1] is set
v + (yy + y1) is Element of the carrier of Y
the addF of Y . (v,(yy + y1)) is Element of the carrier of Y
[v,(yy + y1)] is set
the addF of Y . [v,(yy + y1)] is set
[(K + r),(v + yy)] is Element of [: the carrier of X, the carrier of Y:]
(X,Y) . ([(K + r),(v + yy)],[x1,y1]) is Element of [: the carrier of X, the carrier of Y:]
[[(K + r),(v + yy)],[x1,y1]] is set
(X,Y) . [[(K + r),(v + yy)],[x1,y1]] is set
[((K + r) + x1),((v + yy) + y1)] is Element of [: the carrier of X, the carrier of Y:]
[(r + x1),(yy + y1)] is Element of [: the carrier of X, the carrier of Y:]
(X,Y) . ([K,v],[(r + x1),(yy + y1)]) is Element of [: the carrier of X, the carrier of Y:]
[[K,v],[(r + x1),(yy + y1)]] is set
(X,Y) . [[K,v],[(r + x1),(yy + y1)]] is set
X is non empty right_zeroed addLoopStr
Y is non empty right_zeroed addLoopStr
(X,Y) is non empty strict addLoopStr
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
(X,Y) is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
(X,Y) is Element of [: the carrier of X, the carrier of Y:]
0. X is V52(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. Y is V52(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
addLoopStr(# [: the carrier of X, the carrier of Y:],(X,Y),(X,Y) #) is non empty strict addLoopStr
the carrier of (X,Y) is non empty set
I is Element of the carrier of (X,Y)
0. (X,Y) is V52((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
I + (0. (X,Y)) is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V26([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
the addF of (X,Y) . (I,(0. (X,Y))) is Element of the carrier of (X,Y)
[I,(0. (X,Y))] is set
the addF of (X,Y) . [I,(0. (X,Y))] is set
J is Element of the carrier of X
K is Element of the carrier of Y
[J,K] is Element of [: the carrier of X, the carrier of Y:]
J + (0. X) is Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (J,(0. X)) is Element of the carrier of X
[J,(0. X)] is set
the addF of X . [J,(0. X)] is set
K + (0. Y) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (K,(0. Y)) is Element of the carrier of Y
[K,(0. Y)] is set
the addF of Y . [K,(0. Y)] is set
X is non empty right_complementable addLoopStr
Y is non empty right_complementable addLoopStr
(X,Y) is non empty strict addLoopStr
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
(X,Y) is non empty Relation-like [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] -defined [: the carrier of X, the carrier of Y:] -valued Function-like V26([:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:]) quasi_total Element of bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:]
[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
[:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty Relation-like set
bool [:[:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]:] is non empty set
(X,Y) is Element of [: the carrier of X, the carrier of Y:]
0. X is V52(X) right_complementable Element of the carrier of X
the ZeroF of X is right_complementable Element of the carrier of X
0. Y is V52(Y) right_complementable Element of the carrier of Y
the ZeroF of Y is right_complementable Element of the carrier of Y
[(0. X),(0. Y)] is Element of [: the carrier of X, the carrier of Y:]
addLoopStr(# [: the carrier of X, the carrier of Y:],(X,Y),(X,Y) #) is non empty strict addLoopStr
the carrier of (X,Y) is non empty set
I is Element of the carrier of (X,Y)
J is right_complementable Element of the carrier of X
K is right_complementable Element of the carrier of Y
[J,K] is Element of [: the carrier of X, the carrier of Y:]
K is right_complementable Element of the carrier of X
J + K is right_complementable Element of the carrier of X
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (J,K) is right_complementable Element of the carrier of X
[J,K] is set
the addF of X . [J,K] is set
v is right_complementable Element of the carrier of Y
K + v is right_complementable Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (K,v) is right_complementable Element of the carrier of Y
[K,v] is set
the addF of Y . [K,v] is set
[K,v] is Element of [: the carrier of X, the carrier of Y:]
r is Element of the carrier of (X,Y)
I + r is Element of the carrier of (X,Y)
the addF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like V26([: the carrier of (X,Y), the carrier of (X,Y):]) quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
the addF of (X,Y) . (I,r) is Element of the carrier of (X,Y)
[I,r] is set
the addF of (X,Y) . [I,r] is set
0. (X,Y) is V52((X,Y)) Element of the carrier of (X,Y)
the ZeroF of (X,Y) is Element of the carrier of (X,Y)
J is non empty addLoopStr
the carrier of J is non empty set
K is non empty addLoopStr
the carrier of K is non empty set
yy is non empty addLoopStr
x1 is non empty addLoopStr
(yy,x1) is non empty strict addLoopStr
the carrier of yy is non empty set
the carrier of x1 is non empty set
[: the carrier of yy, the carrier of x1:] is non empty Relation-like set
(yy,x1) is non empty Relation-like [:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:] -defined [: the carrier of yy, the carrier of x1:] -valued Function-like V26([:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:]) quasi_total Element of bool [:[:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:],[: the carrier of yy, the carrier of x1:]:]
[:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:] is non empty Relation-like set
[:[:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:],[: the carrier of yy, the carrier of x1:]:] is non empty Relation-like set
bool [:[:[: the carrier of yy, the carrier of x1:],[: the carrier of yy, the carrier of x1:]:],[: the carrier of yy, the carrier of x1:]:] is non empty set
(yy,x1) is Element of [: the carrier of yy, the carrier of x1:]
0. yy is V52(yy) Element of the carrier of yy
the ZeroF of yy is Element of the carrier of yy
0. x1 is V52(x1) Element of the carrier of x1
the ZeroF of x1 is Element of the carrier of x1
[(0. yy),(0. x1)] is Element of [: the carrier of yy, the carrier of x1:]
addLoopStr(# [: the carrier of yy, the carrier of x1:],(yy,x1),(yy,x1) #) is non empty strict addLoopStr
the carrier of (yy,x1) is non empty set
I is set
X is non empty addLoopStr
Y is non empty addLoopStr
(X,Y) is non empty strict addLoopStr
the carrier of X is non empty set
the carrier of Y is non