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

the empty set is empty set
1 is non empty set

the carrier of R is non empty set
I is Element of the carrier of R
c3 is Element of the carrier of R
I - c3 is Element of the carrier of R
- c3 is Element of the carrier of R
I + (- c3) 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( 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,(- c3)) is Element of the carrier of R
(I - c3) + c3 is Element of the carrier of R
the addF of R . ((I - c3),c3) is Element of the carrier of R
(- c3) + c3 is Element of the carrier of R
the addF of R . ((- c3),c3) is Element of the carrier of R
I + ((- c3) + c3) is Element of the carrier of R
the addF of R . (I,((- c3) + c3)) 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
I + (0. R) is Element of the carrier of R
the addF of R . (I,(0. R)) is Element of the carrier of R

the carrier of R is non empty set
c3 is Element of the carrier of R
I is Element of the carrier of R
I - c3 is Element of the carrier of R
- c3 is Element of the carrier of R
I + (- c3) 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( 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,(- c3)) is Element of the carrier of R
I - (I - c3) is Element of the carrier of R
- (I - c3) is Element of the carrier of R
I + (- (I - c3)) is Element of the carrier of R
the addF of R . (I,(- (I - c3))) is Element of the carrier of R
(I - c3) + c3 is Element of the carrier of R
the addF of R . ((I - c3),c3) is Element of the carrier of R
((I - c3) + c3) - (I - c3) is Element of the carrier of R
((I - c3) + c3) + (- (I - c3)) is Element of the carrier of R
the addF of R . (((I - c3) + c3),(- (I - c3))) is Element of the carrier of R
c3 - (I - c3) is Element of the carrier of R
c3 + (- (I - c3)) is Element of the carrier of R
the addF of R . (c3,(- (I - c3))) is Element of the carrier of R
(c3 - (I - c3)) + (I - c3) is Element of the carrier of R
the addF of R . ((c3 - (I - c3)),(I - c3)) is Element of the carrier of R

the carrier of R is non empty set
I is Element of the carrier of R
c3 is Element of the carrier of R
I - c3 is Element of the carrier of R
- c3 is Element of the carrier of R
I + (- c3) 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( 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,(- c3)) is Element of the carrier of R
x is Element of the carrier of R
x - c3 is Element of the carrier of R
x + (- c3) is Element of the carrier of R
the addF of R . (x,(- c3)) is Element of the carrier of R
(I - c3) - (x - c3) is Element of the carrier of R
- (x - c3) is Element of the carrier of R
(I - c3) + (- (x - c3)) is Element of the carrier of R
the addF of R . ((I - c3),(- (x - c3))) is Element of the carrier of R
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 - c3) - x is Element of the carrier of R
(I - c3) + (- x) is Element of the carrier of R
the addF of R . ((I - c3),(- x)) is Element of the carrier of R
((I - c3) - x) + c3 is Element of the carrier of R
the addF of R . (((I - c3) - x),c3) is Element of the carrier of R
(I - c3) + c3 is Element of the carrier of R
the addF of R . ((I - c3),c3) is Element of the carrier of R
((I - c3) + c3) - x is Element of the carrier of R
((I - c3) + c3) + (- x) is Element of the carrier of R
the addF of R . (((I - c3) + c3),(- x)) is Element of the carrier of R
c3 - c3 is Element of the carrier of R
c3 + (- c3) is Element of the carrier of R
the addF of R . (c3,(- c3)) is Element of the carrier of R
I - (c3 - c3) is Element of the carrier of R
- (c3 - c3) is Element of the carrier of R
I + (- (c3 - c3)) is Element of the carrier of R
the addF of R . (I,(- (c3 - c3))) is Element of the carrier of R
(I - (c3 - c3)) - x is Element of the carrier of R
(I - (c3 - c3)) + (- x) is Element of the carrier of R
the addF of R . ((I - (c3 - c3)),(- 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
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 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
c3 is Element of the carrier of R
I + c3 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( 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,c3) is Element of the carrier of R
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
c3 is Element of the carrier of R
I is Element of the carrier of R
I * c3 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( 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,c3) is Element of the carrier of R
c3 is Element of the carrier of R
I is Element of the carrier of R
c3 * I 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( 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 . (c3,I) is Element of the carrier of R

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
c3 is Element of the carrier of R
I * c3 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( 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,c3) is Element of the carrier of R
I * c3 is Element of the carrier of R

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)
c3 is set
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
c3 is set
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
c3 is set
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

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

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

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
c3 is Element of the carrier of R
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
c3 - x is Element of the carrier of R
- x is Element of the carrier of R
c3 + (- 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 . (c3,(- x)) is Element of the carrier of R
[c3,x] is Element of K33( the carrier of R, the carrier of R)
{c3,x} is non empty set
{c3} is non empty set
{{c3,x},{c3}} is non empty set

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
c3 is Element of the carrier of R
Class ((R,I),c3) is Element of K32( the carrier of R)
{c3} is non empty set
(R,I) .: {c3} is set
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
c3 - x is Element of the carrier of R
- x is Element of the carrier of R
c3 + (- 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 . (c3,(- x)) is Element of the carrier of R

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

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
c3 is set
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
c3 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,([#] R)),(0. R)) is Element of K32( the carrier of R)
{(0. R)} is non empty set
(R,([#] R)) .: {(0. R)} is set

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

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

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

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

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

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

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

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
c3 is Element of the carrier of (R,I)
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

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
c3 is Element of the carrier of R
Class ((R,I),c3) is Element of K32( the carrier of R)
{c3} is non empty set
(R,I) .: {c3} is set
Class (R,I) is non empty V41() a_partition of 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 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
c3 is Element of the carrier of R
Class ((R,I),c3) is Element of K32( the carrier of R)
{c3} is non empty set
(R,I) .: {c3} is set
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
c3 + 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 . (c3,x) is Element of the carrier of R
Class ((R,I),(c3 + x)) is Element of K32( the carrier of R)
{(c3 + x)} is non empty set
(R,I) .: {(c3 + x)} is set
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 - c3 is Element of the carrier of R
- c3 is Element of the carrier of R
B + (- c3) is Element of the carrier of R
the addF of R . (B,(- c3)) is Element of the carrier of R
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 - c3) + (A - x) is Element of the carrier of R
the addF of R . ((B - c3),(A - x)) is Element of the carrier of R
(B - c3) + A is Element of the carrier of R
the addF of R . ((B - c3),A) is Element of the carrier of R
((B - c3) + A) - x is Element of the carrier of R
((B - c3) + A) + (- x) is Element of the carrier of R
the addF of R . (((B - c3) + A),(- x)) is Element of the carrier of R
(B + A) - c3 is Element of the carrier of R
(B + A) + (- c3) is Element of the carrier of R
the addF of R . ((B + A),(- c3)) is Element of the carrier of R
((B + A) - c3) - x is Element of the carrier of R
((B + A) - c3) + (- x) is Element of the carrier of R
the addF of R . (((B + A) - c3),(- x)) is Element of the carrier of R
(B + A) - (c3 + x) is Element of the carrier of R
- (c3 + x) is Element of the carrier of R
(B + A) + (- (c3 + x)) is Element of the carrier of R
the addF of R . ((B + A),(- (c3 + x))) is Element of 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 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
c3 is Element of the carrier of R
Class ((R,I),c3) is Element of K32( the carrier of R)
{c3} is non empty set
(R,I) .: {c3} is set
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
c3 * x 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 . (c3,x) is Element of the carrier of R
Class ((R,I),(c3 * x)) is Element of K32( the carrier of R)
{(c3 * x)} is non empty set
(R,I) .: {(c3 * x)} is set
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 - c3 is Element of the carrier of R
- c3 is Element of the carrier of R
B + (- c3) is Element of the carrier of R
the addF of R . (B,(- c3)) is Element of the carrier of R
(B - c3) * x is Element of the carrier of R
the multF of R . ((B - c3),x) is Element of the carrier of R
B * x is Element of the carrier of R
the multF of R . (B,x) is Element of the carrier of R
(B * x) - (c3 * x) is Element of the carrier of R
- (c3 * x) is Element of the carrier of R
(B * x) + (- (c3 * x)) is Element of the carrier of R
the addF of R . ((B * x),(- (c3 * x))) is Element of the carrier of R
(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 - c3) * x) is Element of the carrier of R
the addF of R . ((B * (A - x)),((B - c3) * x)) is Element of the carrier of R
((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)) - (c3 * x) is Element of the carrier of R
(((B * A) - (B * x)) + (B * x)) + (- (c3 * x)) is Element of the carrier of R
the addF of R . ((((B * A) - (B * x)) + (B * x)),(- (c3 * x))) is Element of the carrier of R
(B * A) - (c3 * x) is Element of the carrier of R
(B * A) + (- (c3 * x)) is Element of the carrier of R
the addF of R . ((B * A),(- (c3 * x))) is Element of the carrier of R
((B - c3) * x) + (B * (A - x)) is Element of the carrier of R
the addF of R . (((B - c3) * x),(B * (A - x))) is Element of 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 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

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)

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