:: PRVECT_3 semantic presentation

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