:: RING_1 semantic presentation

K149() is Element of K32(K145())

K145() is set

K32(K145()) is non empty V33() V35() V36() set

K24() is set

K32(K24()) is non empty V33() V35() V36() set

K32(K149()) is non empty V33() V35() V36() set

{} is empty set

the empty set is empty set

1 is non empty set

field {} is set

R is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V153() V154() V155() V156() addLoopStr

the carrier of R is non empty set

I is Element of the carrier of R

c

I - c

- c

I + (- c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- c

(I - c

the addF of R . ((I - c

(- c

the addF of R . ((- c

I + ((- c

the addF of R . (I,((- c

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

I + (0. R) is Element of the carrier of R

the addF of R . (I,(0. R)) is Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed V153() V154() V155() V156() addLoopStr

the carrier of R is non empty set

c

I is Element of the carrier of R

I - c

- c

I + (- c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- c

I - (I - c

- (I - c

I + (- (I - c

the addF of R . (I,(- (I - c

(I - c

the addF of R . ((I - c

((I - c

((I - c

the addF of R . (((I - c

c

c

the addF of R . (c

(c

the addF of R . ((c

R is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed V153() V154() V155() V156() addLoopStr

the carrier of R is non empty set

I is Element of the carrier of R

c

I - c

- c

I + (- c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- c

x is Element of the carrier of R

x - c

x + (- c

the addF of R . (x,(- c

(I - c

- (x - c

(I - c

the addF of R . ((I - c

I - x is Element of the carrier of R

- x is Element of the carrier of R

I + (- x) is Element of the carrier of R

the addF of R . (I,(- x)) is Element of the carrier of R

(I - c

(I - c

the addF of R . ((I - c

((I - c

the addF of R . (((I - c

(I - c

the addF of R . ((I - c

((I - c

((I - c

the addF of R . (((I - c

c

c

the addF of R . (c

I - (c

- (c

I + (- (c

the addF of R . (I,(- (c

(I - (c

(I - (c

the addF of R . ((I - (c

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

I - (0. R) is Element of the carrier of R

- (0. R) is Element of the carrier of R

I + (- (0. R)) is Element of the carrier of R

the addF of R . (I,(- (0. R))) is Element of the carrier of R

(I - (0. R)) - x is Element of the carrier of R

(I - (0. R)) + (- x) is Element of the carrier of R

the addF of R . ((I - (0. R)),(- x)) is Element of the carrier of R

R is non empty multMagma

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

R is non empty multLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

R is non empty doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

R is non empty doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

R is non empty multLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is Element of K32( the carrier of R)

I is Element of K32( the carrier of R)

R is non empty doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is Element of K32( the carrier of R)

I is Element of K32( the carrier of R)

R is non empty addLoopStr

[#] R is non empty non proper Element of K32( the carrier of R)

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is Element of the carrier of R

c

I + c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,c

R is non empty multMagma

[#] R is non empty non proper Element of K32( the carrier of R)

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

c

I is Element of the carrier of R

I * c

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (I,c

c

I is Element of the carrier of R

c

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (c

R is non empty non degenerated V69() left_add-cancelable right_add-cancelable right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty V21() set

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

{(0. R)} is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

K32( the carrier of R) is non empty V33() V35() V36() set

1_ R is Element of the carrier of R

1. R is V71(R) Element of the carrier of R

the OneF of R is Element of the carrier of R

I is Element of the carrier of R

c

I * c

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (I,c

I * c

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

c

x is set

I is Element of the carrier of R

J is Element of the carrier of R

I - J is Element of the carrier of R

- J is Element of the carrier of R

I + (- J) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- J)) is Element of the carrier of R

J - I is Element of the carrier of R

- I is Element of the carrier of R

J + (- I) is Element of the carrier of R

the addF of R . (J,(- I)) is Element of the carrier of R

- (I - J) is Element of the carrier of R

c

x is set

I is set

J is Element of the carrier of R

B is Element of the carrier of R

J - B is Element of the carrier of R

- B is Element of the carrier of R

J + (- B) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (J,(- B)) is Element of the carrier of R

J is Element of the carrier of R

B is Element of the carrier of R

J - B is Element of the carrier of R

- B is Element of the carrier of R

J + (- B) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (J,(- B)) is Element of the carrier of R

A is Element of the carrier of R

y is Element of the carrier of R

A - y is Element of the carrier of R

- y is Element of the carrier of R

A + (- y) is Element of the carrier of R

the addF of R . (A,(- y)) is Element of the carrier of R

A is Element of the carrier of R

y is Element of the carrier of R

A - y is Element of the carrier of R

- y is Element of the carrier of R

A + (- y) is Element of the carrier of R

the addF of R . (A,(- y)) is Element of the carrier of R

J - y is Element of the carrier of R

J + (- y) is Element of the carrier of R

the addF of R . (J,(- y)) is Element of the carrier of R

B - y is Element of the carrier of R

B + (- y) is Element of the carrier of R

the addF of R . (B,(- y)) is Element of the carrier of R

(J - B) + (B - y) is Element of the carrier of R

the addF of R . ((J - B),(B - y)) is Element of the carrier of R

(J - B) + B is Element of the carrier of R

the addF of R . ((J - B),B) is Element of the carrier of R

((J - B) + B) - y is Element of the carrier of R

((J - B) + B) + (- y) is Element of the carrier of R

the addF of R . (((J - B) + B),(- y)) is Element of the carrier of R

c

x is Element of the carrier of R

x - x is Element of the carrier of R

- x is Element of the carrier of R

x + (- x) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (x,(- x)) is Element of the carrier of R

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

c

x is Element of the carrier of R

I is Element of the carrier of R

[x,I] is Element of K33( the carrier of R, the carrier of R)

{x,I} is non empty set

{x} is non empty set

{{x,I},{x}} is non empty set

x - I is Element of the carrier of R

- I is Element of the carrier of R

x + (- I) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (x,(- I)) is Element of the carrier of R

J is Element of the carrier of R

B is Element of the carrier of R

J - B is Element of the carrier of R

- B is Element of the carrier of R

J + (- B) is Element of the carrier of R

the addF of R . (J,(- B)) is Element of the carrier of R

c

x is Relation-like the carrier of R -defined the carrier of R -valued Element of K32(K33( the carrier of R, the carrier of R))

I is set

J is set

[I,J] is set

{I,J} is non empty set

{I} is non empty set

{{I,J},{I}} is non empty set

B is Element of the carrier of R

A is Element of the carrier of R

B - A is Element of the carrier of R

- A is Element of the carrier of R

B + (- A) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (B,(- A)) is Element of the carrier of R

B is Element of the carrier of R

A is Element of the carrier of R

B - A is Element of the carrier of R

- A is Element of the carrier of R

B + (- A) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (B,(- A)) is Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

x is Relation-like the carrier of R -defined the carrier of R -valued total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

I is set

J is set

[I,J] is set

{I,J} is non empty set

{I} is non empty set

{{I,J},{I}} is non empty set

B is Element of the carrier of R

A is Element of the carrier of R

B - A is Element of the carrier of R

- A is Element of the carrier of R

B + (- A) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (B,(- A)) is Element of the carrier of R

B is Element of the carrier of R

A is Element of the carrier of R

B - A is Element of the carrier of R

- A is Element of the carrier of R

B + (- A) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (B,(- A)) is Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

c

x is Element of the carrier of R

Class ((R,I),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,I) .: {x} is set

c

- x is Element of the carrier of R

c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (c

[c

{c

{c

{{c

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

c

Class ((R,I),c

{c

(R,I) .: {c

x is Element of the carrier of R

Class ((R,I),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,I) .: {x} is set

c

- x is Element of the carrier of R

c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (c

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

[#] R is non empty non proper add-closed left-ideal right-ideal Element of K32( the carrier of R)

K32( the carrier of R) is non empty V33() V35() V36() set

(R,([#] R)) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

I is Element of the carrier of R

Class ((R,([#] R)),I) is Element of K32( the carrier of R)

{I} is non empty set

(R,([#] R)) .: {I} is set

x is set

I is Element of the carrier of R

I - I is Element of the carrier of R

- I is Element of the carrier of R

I + (- I) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- I)) is Element of the carrier of R

[I,I] is Element of K33( the carrier of R, the carrier of R)

{I,I} is non empty set

{I} is non empty set

{{I,I},{I}} is non empty set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

[#] R is non empty non proper add-closed left-ideal right-ideal Element of K32( the carrier of R)

K32( the carrier of R) is non empty V33() V35() V36() set

(R,([#] R)) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

Class (R,([#] R)) is non empty V41() a_partition of the carrier of R

{ the carrier of R} is non empty set

c

x is set

Class ((R,([#] R)),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,([#] R)) .: {x} is set

I is Element of the carrier of R

Class ((R,([#] R)),I) is Element of K32( the carrier of R)

{I} is non empty set

(R,([#] R)) .: {I} is set

J is set

B is Element of the carrier of R

B - I is Element of the carrier of R

- I is Element of the carrier of R

B + (- I) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (B,(- I)) is Element of the carrier of R

[B,I] is Element of K33( the carrier of R, the carrier of R)

{B,I} is non empty set

{B} is non empty set

{{B,I},{B}} is non empty set

c

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

Class ((R,([#] R)),(0. R)) is Element of K32( the carrier of R)

{(0. R)} is non empty set

(R,([#] R)) .: {(0. R)} is set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

{(0. R)} is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

K32( the carrier of R) is non empty V33() V35() V36() set

(R,{(0. R)}) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

I is Element of the carrier of R

Class ((R,{(0. R)}),I) is Element of K32( the carrier of R)

{I} is non empty set

(R,{(0. R)}) .: {I} is set

{I} is non empty Element of K32( the carrier of R)

x is set

I is Element of the carrier of R

[I,I] is Element of K33( the carrier of R, the carrier of R)

{I,I} is non empty set

{I} is non empty set

{{I,I},{I}} is non empty set

I - I is Element of the carrier of R

- I is Element of the carrier of R

I + (- I) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- I)) is Element of the carrier of R

x is set

I - I is Element of the carrier of R

- I is Element of the carrier of R

I + (- I) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (I,(- I)) is Element of the carrier of R

[x,I] is set

{x,I} is non empty set

{x} is non empty set

{{x,I},{x}} is non empty set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

{(0. R)} is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

K32( the carrier of R) is non empty V33() V35() V36() set

(R,{(0. R)}) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

Class (R,{(0. R)}) is non empty V41() a_partition of the carrier of R

singleton the carrier of R is Relation-like the carrier of R -defined K110( the carrier of R) -valued Function-like V27( the carrier of R,K110( the carrier of R)) Element of K32(K33( the carrier of R,K110( the carrier of R)))

K110( the carrier of R) is non empty V33() V35() V36() set

K33( the carrier of R,K110( the carrier of R)) is non empty set

K32(K33( the carrier of R,K110( the carrier of R))) is non empty V33() V35() V36() set

rng (singleton the carrier of R) is set

dom (singleton the carrier of R) is Element of K32( the carrier of R)

x is set

I is set

Class ((R,{(0. R)}),I) is Element of K32( the carrier of R)

{I} is non empty set

(R,{(0. R)}) .: {I} is set

J is Element of the carrier of R

Class ((R,{(0. R)}),J) is Element of K32( the carrier of R)

{J} is non empty set

(R,{(0. R)}) .: {J} is set

{J} is non empty Element of K32( the carrier of R)

B is set

A is Element of the carrier of R

[A,J] is Element of K33( the carrier of R, the carrier of R)

{A,J} is non empty set

{A} is non empty set

{{A,J},{A}} is non empty set

A - J is Element of the carrier of R

- J is Element of the carrier of R

A + (- J) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (A,(- J)) is Element of the carrier of R

B is set

J - J is Element of the carrier of R

- J is Element of the carrier of R

J + (- J) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (J,(- J)) is Element of the carrier of R

[B,J] is set

{B,J} is non empty set

{B} is non empty set

{{B,J},{B}} is non empty set

(singleton the carrier of R) . J is set

x is set

I is set

(singleton the carrier of R) . I is set

{I} is non empty set

Class ((R,{(0. R)}),I) is Element of K32( the carrier of R)

(R,{(0. R)}) .: {I} is set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

Class (R,I) is non empty V41() a_partition of the carrier of R

1. R is Element of the carrier of R

the OneF of R is Element of the carrier of R

Class ((R,I),(1. R)) is Element of K32( the carrier of R)

{(1. R)} is non empty set

(R,I) .: {(1. R)} is set

0. R is V71(R) Element of the carrier of R

the ZeroF of R is Element of the carrier of R

Class ((R,I),(0. R)) is Element of K32( the carrier of R)

{(0. R)} is non empty set

(R,I) .: {(0. R)} is set

1_ R is Element of the carrier of R

Class ((R,I),(1_ R)) is Element of K32( the carrier of R)

{(1_ R)} is non empty set

(R,I) .: {(1_ R)} is set

B is Element of Class (R,I)

A is Element of Class (R,I)

y is set

Class ((R,I),y) is Element of K32( the carrier of R)

{y} is non empty set

(R,I) .: {y} is set

Aa is set

Class ((R,I),Aa) is Element of K32( the carrier of R)

{Aa} is non empty set

(R,I) .: {Aa} is set

Ab is Element of the carrier of R

rd is Element of the carrier of R

Ab + rd is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (Ab,rd) is Element of the carrier of R

Class ((R,I),(Ab + rd)) is Element of K32( the carrier of R)

{(Ab + rd)} is non empty set

(R,I) .: {(Ab + rd)} is set

K33((Class (R,I)),(Class (R,I))) is non empty set

K33(K33((Class (R,I)),(Class (R,I))),(Class (R,I))) is non empty set

K32(K33(K33((Class (R,I)),(Class (R,I))),(Class (R,I)))) is non empty V33() V35() V36() set

B is Relation-like K33((Class (R,I)),(Class (R,I))) -defined Class (R,I) -valued Function-like V27(K33((Class (R,I)),(Class (R,I))), Class (R,I)) Element of K32(K33(K33((Class (R,I)),(Class (R,I))),(Class (R,I))))

A is Element of Class (R,I)

y is Element of Class (R,I)

Aa is set

Class ((R,I),Aa) is Element of K32( the carrier of R)

{Aa} is non empty set

(R,I) .: {Aa} is set

Ab is set

Class ((R,I),Ab) is Element of K32( the carrier of R)

{Ab} is non empty set

(R,I) .: {Ab} is set

rd is Element of the carrier of R

sd is Element of the carrier of R

rd * sd is Element of the carrier of R

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (rd,sd) is Element of the carrier of R

Class ((R,I),(rd * sd)) is Element of K32( the carrier of R)

{(rd * sd)} is non empty set

(R,I) .: {(rd * sd)} is set

A is Relation-like K33((Class (R,I)),(Class (R,I))) -defined Class (R,I) -valued Function-like V27(K33((Class (R,I)),(Class (R,I))), Class (R,I)) Element of K32(K33(K33((Class (R,I)),(Class (R,I))),(Class (R,I))))

I is Element of Class (R,I)

J is Element of Class (R,I)

doubleLoopStr(# (Class (R,I)),B,A,I,J #) is strict doubleLoopStr

the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #) is set

1. doubleLoopStr(# (Class (R,I)),B,A,I,J #) is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

the OneF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

0. doubleLoopStr(# (Class (R,I)),B,A,I,J #) is V71( doubleLoopStr(# (Class (R,I)),B,A,I,J #)) Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

the ZeroF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

the addF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) is Relation-like K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) -defined the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #) -valued Function-like V27(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) Element of K32(K33(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)))

K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) is set

K33(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) is set

K32(K33(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #))) is non empty V33() V35() V36() set

the multF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) is Relation-like K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) -defined the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #) -valued Function-like V27(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)) Element of K32(K33(K33( the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)), the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)))

y is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

Aa is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

the addF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) . (y,Aa) is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

Ab is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

rd is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

the multF of doubleLoopStr(# (Class (R,I)),B,A,I,J #) . (Ab,rd) is Element of the carrier of doubleLoopStr(# (Class (R,I)),B,A,I,J #)

x is strict doubleLoopStr

the carrier of x is set

1. x is Element of the carrier of x

the OneF of x is Element of the carrier of x

0. x is V71(x) Element of the carrier of x

the ZeroF of x is Element of the carrier of x

the addF of x is Relation-like K33( the carrier of x, the carrier of x) -defined the carrier of x -valued Function-like V27(K33( the carrier of x, the carrier of x), the carrier of x) Element of K32(K33(K33( the carrier of x, the carrier of x), the carrier of x))

K33( the carrier of x, the carrier of x) is set

K33(K33( the carrier of x, the carrier of x), the carrier of x) is set

K32(K33(K33( the carrier of x, the carrier of x), the carrier of x)) is non empty V33() V35() V36() set

the multF of x is Relation-like K33( the carrier of x, the carrier of x) -defined the carrier of x -valued Function-like V27(K33( the carrier of x, the carrier of x), the carrier of x) Element of K32(K33(K33( the carrier of x, the carrier of x), the carrier of x))

I is strict doubleLoopStr

the carrier of I is set

1. I is Element of the carrier of I

the OneF of I is Element of the carrier of I

0. I is V71(I) Element of the carrier of I

the ZeroF of I is Element of the carrier of I

the addF of I is Relation-like K33( the carrier of I, the carrier of I) -defined the carrier of I -valued Function-like V27(K33( the carrier of I, the carrier of I), the carrier of I) Element of K32(K33(K33( the carrier of I, the carrier of I), the carrier of I))

K33( the carrier of I, the carrier of I) is set

K33(K33( the carrier of I, the carrier of I), the carrier of I) is set

K32(K33(K33( the carrier of I, the carrier of I), the carrier of I)) is non empty V33() V35() V36() set

the multF of I is Relation-like K33( the carrier of I, the carrier of I) -defined the carrier of I -valued Function-like V27(K33( the carrier of I, the carrier of I), the carrier of I) Element of K32(K33(K33( the carrier of I, the carrier of I), the carrier of I))

J is Element of the carrier of x

B is Element of the carrier of x

the multF of x . (J,B) is Element of the carrier of x

the multF of I . (J,B) is set

A is Element of the carrier of R

Class ((R,I),A) is Element of K32( the carrier of R)

{A} is non empty set

(R,I) .: {A} is set

y is Element of the carrier of R

Class ((R,I),y) is Element of K32( the carrier of R)

{y} is non empty set

(R,I) .: {y} is set

A * y is Element of the carrier of R

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (A,y) is Element of the carrier of R

Class ((R,I),(A * y)) is Element of K32( the carrier of R)

{(A * y)} is non empty set

(R,I) .: {(A * y)} is set

Aa is Element of the carrier of R

Class ((R,I),Aa) is Element of K32( the carrier of R)

{Aa} is non empty set

(R,I) .: {Aa} is set

Ab is Element of the carrier of R

Class ((R,I),Ab) is Element of K32( the carrier of R)

{Ab} is non empty set

(R,I) .: {Ab} is set

Aa * Ab is Element of the carrier of R

the multF of R . (Aa,Ab) is Element of the carrier of R

Class ((R,I),(Aa * Ab)) is Element of K32( the carrier of R)

{(Aa * Ab)} is non empty set

(R,I) .: {(Aa * Ab)} is set

y - Ab is Element of the carrier of R

- Ab is Element of the carrier of R

y + (- Ab) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

the addF of R . (y,(- Ab)) is Element of the carrier of R

Aa * (y - Ab) is Element of the carrier of R

the multF of R . (Aa,(y - Ab)) is Element of the carrier of R

A - Aa is Element of the carrier of R

- Aa is Element of the carrier of R

A + (- Aa) is Element of the carrier of R

the addF of R . (A,(- Aa)) is Element of the carrier of R

(A - Aa) * y is Element of the carrier of R

the multF of R . ((A - Aa),y) is Element of the carrier of R

((A - Aa) * y) + (Aa * (y - Ab)) is Element of the carrier of R

the addF of R . (((A - Aa) * y),(Aa * (y - Ab))) is Element of the carrier of R

Aa * y is Element of the carrier of R

the multF of R . (Aa,y) is Element of the carrier of R

(A * y) - (Aa * y) is Element of the carrier of R

- (Aa * y) is Element of the carrier of R

(A * y) + (- (Aa * y)) is Element of the carrier of R

the addF of R . ((A * y),(- (Aa * y))) is Element of the carrier of R

((A * y) - (Aa * y)) + (Aa * (y - Ab)) is Element of the carrier of R

the addF of R . (((A * y) - (Aa * y)),(Aa * (y - Ab))) is Element of the carrier of R

(Aa * y) - (Aa * Ab) is Element of the carrier of R

- (Aa * Ab) is Element of the carrier of R

(Aa * y) + (- (Aa * Ab)) is Element of the carrier of R

the addF of R . ((Aa * y),(- (Aa * Ab))) is Element of the carrier of R

((A * y) - (Aa * y)) + ((Aa * y) - (Aa * Ab)) is Element of the carrier of R

the addF of R . (((A * y) - (Aa * y)),((Aa * y) - (Aa * Ab))) is Element of the carrier of R

((A * y) - (Aa * y)) + (Aa * y) is Element of the carrier of R

the addF of R . (((A * y) - (Aa * y)),(Aa * y)) is Element of the carrier of R

(((A * y) - (Aa * y)) + (Aa * y)) - (Aa * Ab) is Element of the carrier of R

(((A * y) - (Aa * y)) + (Aa * y)) + (- (Aa * Ab)) is Element of the carrier of R

the addF of R . ((((A * y) - (Aa * y)) + (Aa * y)),(- (Aa * Ab))) is Element of the carrier of R

(A * y) - (Aa * Ab) is Element of the carrier of R

(A * y) + (- (Aa * Ab)) is Element of the carrier of R

the addF of R . ((A * y),(- (Aa * Ab))) is Element of the carrier of R

J is Element of the carrier of x

B is Element of the carrier of x

the addF of x . (J,B) is Element of the carrier of x

the addF of I . (J,B) is set

A is Element of the carrier of R

Class ((R,I),A) is Element of K32( the carrier of R)

{A} is non empty set

(R,I) .: {A} is set

y is Element of the carrier of R

Class ((R,I),y) is Element of K32( the carrier of R)

{y} is non empty set

(R,I) .: {y} is set

A + y is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (A,y) is Element of the carrier of R

Class ((R,I),(A + y)) is Element of K32( the carrier of R)

{(A + y)} is non empty set

(R,I) .: {(A + y)} is set

Aa is Element of the carrier of R

Class ((R,I),Aa) is Element of K32( the carrier of R)

{Aa} is non empty set

(R,I) .: {Aa} is set

Ab is Element of the carrier of R

Class ((R,I),Ab) is Element of K32( the carrier of R)

{Ab} is non empty set

(R,I) .: {Ab} is set

Aa + Ab is Element of the carrier of R

the addF of R . (Aa,Ab) is Element of the carrier of R

Class ((R,I),(Aa + Ab)) is Element of K32( the carrier of R)

{(Aa + Ab)} is non empty set

(R,I) .: {(Aa + Ab)} is set

A - Aa is Element of the carrier of R

- Aa is Element of the carrier of R

A + (- Aa) is Element of the carrier of R

the addF of R . (A,(- Aa)) is Element of the carrier of R

y - Ab is Element of the carrier of R

- Ab is Element of the carrier of R

y + (- Ab) is Element of the carrier of R

the addF of R . (y,(- Ab)) is Element of the carrier of R

(A - Aa) + (y - Ab) is Element of the carrier of R

the addF of R . ((A - Aa),(y - Ab)) is Element of the carrier of R

(A + y) - (Aa + Ab) is Element of the carrier of R

- (Aa + Ab) is Element of the carrier of R

(A + y) + (- (Aa + Ab)) is Element of the carrier of R

the addF of R . ((A + y),(- (Aa + Ab))) is Element of the carrier of R

(A + y) - Aa is Element of the carrier of R

(A + y) + (- Aa) is Element of the carrier of R

the addF of R . ((A + y),(- Aa)) is Element of the carrier of R

((A + y) - Aa) - Ab is Element of the carrier of R

((A + y) - Aa) + (- Ab) is Element of the carrier of R

the addF of R . (((A + y) - Aa),(- Ab)) is Element of the carrier of R

(A - Aa) + y is Element of the carrier of R

the addF of R . ((A - Aa),y) is Element of the carrier of R

((A - Aa) + y) - Ab is Element of the carrier of R

((A - Aa) + y) + (- Ab) is Element of the carrier of R

the addF of R . (((A - Aa) + y),(- Ab)) is Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is strict doubleLoopStr

the carrier of (R,I) is set

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

Class (R,I) is non empty V41() a_partition of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is non empty strict doubleLoopStr

the carrier of (R,I) is non empty set

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

c

Class (R,I) is non empty V41() a_partition of the carrier of R

x is set

Class ((R,I),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,I) .: {x} is set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

(R,I) is non empty strict doubleLoopStr

the carrier of (R,I) is non empty set

c

Class ((R,I),c

{c

(R,I) .: {c

Class (R,I) is non empty V41() a_partition of the carrier of R

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is non empty strict doubleLoopStr

the carrier of (R,I) is non empty set

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

c

Class ((R,I),c

{c

(R,I) .: {c

x is Element of the carrier of R

Class ((R,I),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,I) .: {x} is set

c

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (c

Class ((R,I),(c

{(c

(R,I) .: {(c

I is Element of the carrier of (R,I)

J is Element of the carrier of (R,I)

I + J is Element of the carrier of (R,I)

the addF of (R,I) is Relation-like K33( the carrier of (R,I), the carrier of (R,I)) -defined the carrier of (R,I) -valued Function-like V27(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) Element of K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)))

K33( the carrier of (R,I), the carrier of (R,I)) is non empty set

K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) is non empty set

K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I))) is non empty V33() V35() V36() set

the addF of (R,I) . (I,J) is Element of the carrier of (R,I)

B is Element of the carrier of R

Class ((R,I),B) is Element of K32( the carrier of R)

{B} is non empty set

(R,I) .: {B} is set

A is Element of the carrier of R

Class ((R,I),A) is Element of K32( the carrier of R)

{A} is non empty set

(R,I) .: {A} is set

B + A is Element of the carrier of R

the addF of R . (B,A) is Element of the carrier of R

Class ((R,I),(B + A)) is Element of K32( the carrier of R)

{(B + A)} is non empty set

(R,I) .: {(B + A)} is set

B - c

- c

B + (- c

the addF of R . (B,(- c

A - x is Element of the carrier of R

- x is Element of the carrier of R

A + (- x) is Element of the carrier of R

the addF of R . (A,(- x)) is Element of the carrier of R

(B - c

the addF of R . ((B - c

(B - c

the addF of R . ((B - c

((B - c

((B - c

the addF of R . (((B - c

(B + A) - c

(B + A) + (- c

the addF of R . ((B + A),(- c

((B + A) - c

((B + A) - c

the addF of R . (((B + A) - c

(B + A) - (c

- (c

(B + A) + (- (c

the addF of R . ((B + A),(- (c

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is non empty strict doubleLoopStr

the carrier of (R,I) is non empty set

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

c

Class ((R,I),c

{c

(R,I) .: {c

x is Element of the carrier of R

Class ((R,I),x) is Element of K32( the carrier of R)

{x} is non empty set

(R,I) .: {x} is set

c

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the multF of R . (c

Class ((R,I),(c

{(c

(R,I) .: {(c

I is Element of the carrier of (R,I)

J is Element of the carrier of (R,I)

I * J is Element of the carrier of (R,I)

the multF of (R,I) is Relation-like K33( the carrier of (R,I), the carrier of (R,I)) -defined the carrier of (R,I) -valued Function-like V27(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) Element of K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)))

K33( the carrier of (R,I), the carrier of (R,I)) is non empty set

K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) is non empty set

K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I))) is non empty V33() V35() V36() set

the multF of (R,I) . (I,J) is Element of the carrier of (R,I)

B is Element of the carrier of R

Class ((R,I),B) is Element of K32( the carrier of R)

{B} is non empty set

(R,I) .: {B} is set

A is Element of the carrier of R

Class ((R,I),A) is Element of K32( the carrier of R)

{A} is non empty set

(R,I) .: {A} is set

B * A is Element of the carrier of R

the multF of R . (B,A) is Element of the carrier of R

Class ((R,I),(B * A)) is Element of K32( the carrier of R)

{(B * A)} is non empty set

(R,I) .: {(B * A)} is set

A - x is Element of the carrier of R

- x is Element of the carrier of R

A + (- x) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

the addF of R . (A,(- x)) is Element of the carrier of R

B * (A - x) is Element of the carrier of R

the multF of R . (B,(A - x)) is Element of the carrier of R

B - c

- c

B + (- c

the addF of R . (B,(- c

(B - c

the multF of R . ((B - c

B * x is Element of the carrier of R

the multF of R . (B,x) is Element of the carrier of R

(B * x) - (c

- (c

(B * x) + (- (c

the addF of R . ((B * x),(- (c

(B * A) - (B * x) is Element of the carrier of R

- (B * x) is Element of the carrier of R

(B * A) + (- (B * x)) is Element of the carrier of R

the addF of R . ((B * A),(- (B * x))) is Element of the carrier of R

(B * (A - x)) + ((B - c

the addF of R . ((B * (A - x)),((B - c

((B * A) - (B * x)) + (B * x) is Element of the carrier of R

the addF of R . (((B * A) - (B * x)),(B * x)) is Element of the carrier of R

(((B * A) - (B * x)) + (B * x)) - (c

(((B * A) - (B * x)) + (B * x)) + (- (c

the addF of R . ((((B * A) - (B * x)) + (B * x)),(- (c

(B * A) - (c

(B * A) + (- (c

the addF of R . ((B * A),(- (c

((B - c

the addF of R . (((B - c

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

(R,I) is non empty strict doubleLoopStr

the carrier of (R,I) is non empty set

x is Element of the carrier of (R,I)

1_ R is Element of the carrier of R

1. R is Element of the carrier of R

the OneF of R is Element of the carrier of R

Class ((R,I),(1_ R)) is Element of K32( the carrier of R)

{(1_ R)} is non empty set

(R,I) .: {(1_ R)} is set

J is Element of the carrier of R

Class ((R,I),J) is Element of K32( the carrier of R)

{J} is non empty set

(R,I) .: {J} is set

I is Element of the carrier of (R,I)

B is Element of the carrier of R

Class ((R,I),B) is Element of K32( the carrier of R)

{B} is non empty set

(R,I) .: {B} is set

J - (1_ R) is Element of the carrier of R

- (1_ R) is Element of the carrier of R

J + (- (1_ R)) is Element of the carrier of R

the addF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

K33(K33( the carrier of R, the carrier of R), the carrier of R) is non empty set

K32(K33(K33( the carrier of R, the carrier of R), the carrier of R)) is non empty V33() V35() V36() set

the addF of R . (J,(- (1_ R))) is Element of the carrier of R

(J - (1_ R)) * B is Element of the carrier of R

the multF of R is Relation-like K33( the carrier of R, the carrier of R) -defined the carrier of R -valued Function-like V27(K33( the carrier of R, the carrier of R), the carrier of R) Element of K32(K33(K33( the carrier of R, the carrier of R), the carrier of R))

the multF of R . ((J - (1_ R)),B) is Element of the carrier of R

B * (J - (1_ R)) is Element of the carrier of R

the multF of R . (B,(J - (1_ R))) is Element of the carrier of R

B * J is Element of the carrier of R

the multF of R . (B,J) is Element of the carrier of R

B * (1_ R) is Element of the carrier of R

the multF of R . (B,(1_ R)) is Element of the carrier of R

(B * J) - (B * (1_ R)) is Element of the carrier of R

- (B * (1_ R)) is Element of the carrier of R

(B * J) + (- (B * (1_ R))) is Element of the carrier of R

the addF of R . ((B * J),(- (B * (1_ R)))) is Element of the carrier of R

(B * J) - B is Element of the carrier of R

- B is Element of the carrier of R

(B * J) + (- B) is Element of the carrier of R

the addF of R . ((B * J),(- B)) is Element of the carrier of R

I * x is Element of the carrier of (R,I)

the multF of (R,I) is Relation-like K33( the carrier of (R,I), the carrier of (R,I)) -defined the carrier of (R,I) -valued Function-like V27(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) Element of K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)))

K33( the carrier of (R,I), the carrier of (R,I)) is non empty set

K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) is non empty set

K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I))) is non empty V33() V35() V36() set

the multF of (R,I) . (I,x) is Element of the carrier of (R,I)

Class ((R,I),(B * J)) is Element of K32( the carrier of R)

{(B * J)} is non empty set

(R,I) .: {(B * J)} is set

J * B is Element of the carrier of R

the multF of R . (J,B) is Element of the carrier of R

(1_ R) * B is Element of the carrier of R

the multF of R . ((1_ R),B) is Element of the carrier of R

(J * B) - ((1_ R) * B) is Element of the carrier of R

- ((1_ R) * B) is Element of the carrier of R

(J * B) + (- ((1_ R) * B)) is Element of the carrier of R

the addF of R . ((J * B),(- ((1_ R) * B))) is Element of the carrier of R

(J * B) - B is Element of the carrier of R

(J * B) + (- B) is Element of the carrier of R

the addF of R . ((J * B),(- B)) is Element of the carrier of R

x * I is Element of the carrier of (R,I)

the multF of (R,I) . (x,I) is Element of the carrier of (R,I)

Class ((R,I),(J * B)) is Element of K32( the carrier of R)

{(J * B)} is non empty set

(R,I) .: {(J * B)} is set

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is Relation-like the carrier of R -defined the carrier of R -valued non empty total symmetric transitive Element of K32(K33( the carrier of R, the carrier of R))

K33( the carrier of R, the carrier of R) is non empty set

K32(K33( the carrier of R, the carrier of R)) is non empty V33() V35() V36() set

1. R is Element of the carrier of R

the OneF of R is Element of the carrier of R

Class ((R,I),(1. R)) is Element of K32( the carrier of R)

{(1. R)} is non empty set

(R,I) .: {(1. R)} is set

(R,I) is non empty strict doubleLoopStr

1. (R,I) is Element of the carrier of (R,I)

the carrier of (R,I) is non empty set

the OneF of (R,I) is Element of the carrier of (R,I)

R is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr

the carrier of R is non empty set

K32( the carrier of R) is non empty V33() V35() V36() set

I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)

(R,I) is non empty strict doubleLoopStr

the addF of (R,I) is Relation-like K33( the carrier of (R,I), the carrier of (R,I)) -defined the carrier of (R,I) -valued Function-like V27(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) Element of K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)))

the carrier of (R,I) is non empty set

K33( the carrier of (R,I), the carrier of (R,I)) is non empty set

K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I)) is non empty set

K32(K33(K33( the carrier of (R,I), the carrier of (R,I)), the carrier of (R,I))) is non empty V33() V35() V36()