:: 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₃ is Element of the carrier of R
I - c₃ is Element of the carrier of R
- c₃ is Element of the carrier of R
I + (- c₃) 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,(- c₃)) is Element of the carrier of R
(I - c₃) + c₃ is Element of the carrier of R
the addF of R . ((I - c₃),c₃) is Element of the carrier of R
(- c₃) + c₃ is Element of the carrier of R
the addF of R . ((- c₃),c₃) is Element of the carrier of R
I + ((- c₃) + c₃) is Element of the carrier of R
the addF of R . (I,((- c₃) + c₃)) 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
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₃ is Element of the carrier of R
I is Element of the carrier of R
I - c₃ is Element of the carrier of R
- c₃ is Element of the carrier of R
I + (- c₃) 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,(- c₃)) is Element of the carrier of R
I - (I - c₃) is Element of the carrier of R
- (I - c₃) is Element of the carrier of R
I + (- (I - c₃)) is Element of the carrier of R
the addF of R . (I,(- (I - c₃))) is Element of the carrier of R
(I - c₃) + c₃ is Element of the carrier of R
the addF of R . ((I - c₃),c₃) is Element of the carrier of R
((I - c₃) + c₃) - (I - c₃) is Element of the carrier of R
((I - c₃) + c₃) + (- (I - c₃)) is Element of the carrier of R
the addF of R . (((I - c₃) + c₃),(- (I - c₃))) is Element of the carrier of R
c₃ - (I - c₃) is Element of the carrier of R
c₃ + (- (I - c₃)) is Element of the carrier of R
the addF of R . (c₃,(- (I - c₃))) is Element of the carrier of R
(c₃ - (I - c₃)) + (I - c₃) is Element of the carrier of R
the addF of R . ((c₃ - (I - c₃)),(I - c₃)) 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
I is Element of the carrier of R
c₃ is Element of the carrier of R
I - c₃ is Element of the carrier of R
- c₃ is Element of the carrier of R
I + (- c₃) 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,(- c₃)) is Element of the carrier of R
x is Element of the carrier of R
x - c₃ is Element of the carrier of R
x + (- c₃) is Element of the carrier of R
the addF of R . (x,(- c₃)) is Element of the carrier of R
(I - c₃) - (x - c₃) is Element of the carrier of R
- (x - c₃) is Element of the carrier of R
(I - c₃) + (- (x - c₃)) is Element of the carrier of R
the addF of R . ((I - c₃),(- (x - c₃))) 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 - c₃) - x is Element of the carrier of R
(I - c₃) + (- x) is Element of the carrier of R
the addF of R . ((I - c₃),(- x)) is Element of the carrier of R
((I - c₃) - x) + c₃ is Element of the carrier of R
the addF of R . (((I - c₃) - x),c₃) is Element of the carrier of R
(I - c₃) + c₃ is Element of the carrier of R
the addF of R . ((I - c₃),c₃) is Element of the carrier of R
((I - c₃) + c₃) - x is Element of the carrier of R
((I - c₃) + c₃) + (- x) is Element of the carrier of R
the addF of R . (((I - c₃) + c₃),(- x)) is Element of the carrier of R
c₃ - c₃ is Element of the carrier of R
c₃ + (- c₃) is Element of the carrier of R
the addF of R . (c₃,(- c₃)) is Element of the carrier of R
I - (c₃ - c₃) is Element of the carrier of R
- (c₃ - c₃) is Element of the carrier of R
I + (- (c₃ - c₃)) is Element of the carrier of R
the addF of R . (I,(- (c₃ - c₃))) is Element of the carrier of R
(I - (c₃ - c₃)) - x is Element of the carrier of R
(I - (c₃ - c₃)) + (- x) is Element of the carrier of R
the addF of R . ((I - (c₃ - c₃)),(- 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 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₃ is Element of the carrier of R
I + c₃ 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,c₃) 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
c₃ is Element of the carrier of R
I is Element of the carrier of R
I * c₃ 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,c₃) is Element of the carrier of R
c₃ is Element of the carrier of R
I is Element of the carrier of R
c₃ * 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 . (c₃,I) is Element of the carrier of R
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₃ is Element of the carrier of R
I * c₃ 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,c₃) is Element of the carrier of R
I * c₃ 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₃ 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
c₃ 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
c₃ 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
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₃ 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
c₃ 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
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₃ 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
c₃ - x is Element of the carrier of R
- x is Element of the carrier of R
c₃ + (- 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 . (c₃,(- x)) is Element of the carrier of R
[c₃,x] is Element of K33( the carrier of R, the carrier of R)
{c₃,x} is non empty set
{c₃} is non empty set
{{c₃,x},{c₃}} 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
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₃ is Element of the carrier of R
Class ((R,I),c₃) is Element of K32( the carrier of R)
{c₃} is non empty set
(R,I) .: {c₃} 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
c₃ - x is Element of the carrier of R
- x is Element of the carrier of R
c₃ + (- 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 . (c₃,(- x)) 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
[#] 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₃ 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
c₃ 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
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₃ 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
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₃ is Element of the carrier of R
Class ((R,I),c₃) is Element of K32( the carrier of R)
{c₃} is non empty set
(R,I) .: {c₃} is 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₃ is Element of the carrier of R
Class ((R,I),c₃) is Element of K32( the carrier of R)
{c₃} is non empty set
(R,I) .: {c₃} 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
c₃ + 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 . (c₃,x) is Element of the carrier of R
Class ((R,I),(c₃ + x)) is Element of K32( the carrier of R)
{(c₃ + x)} is non empty set
(R,I) .: {(c₃ + 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 - c₃ is Element of the carrier of R
- c₃ is Element of the carrier of R
B + (- c₃) is Element of the carrier of R
the addF of R . (B,(- c₃)) 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 - c₃) + (A - x) is Element of the carrier of R
the addF of R . ((B - c₃),(A - x)) is Element of the carrier of R
(B - c₃) + A is Element of the carrier of R
the addF of R . ((B - c₃),A) is Element of the carrier of R
((B - c₃) + A) - x is Element of the carrier of R
((B - c₃) + A) + (- x) is Element of the carrier of R
the addF of R . (((B - c₃) + A),(- x)) is Element of the carrier of R
(B + A) - c₃ is Element of the carrier of R
(B + A) + (- c₃) is Element of the carrier of R
the addF of R . ((B + A),(- c₃)) is Element of the carrier of R
((B + A) - c₃) - x is Element of the carrier of R
((B + A) - c₃) + (- x) is Element of the carrier of R
the addF of R . (((B + A) - c₃),(- x)) is Element of the carrier of R
(B + A) - (c₃ + x) is Element of the carrier of R
- (c₃ + x) is Element of the carrier of R
(B + A) + (- (c₃ + x)) is Element of the carrier of R
the addF of R . ((B + A),(- (c₃ + x))) 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 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₃ is Element of the carrier of R
Class ((R,I),c₃) is Element of K32( the carrier of R)
{c₃} is non empty set
(R,I) .: {c₃} 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
c₃ * 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 . (c₃,x) is Element of the carrier of R
Class ((R,I),(c₃ * x)) is Element of K32( the carrier of R)
{(c₃ * x)} is non empty set
(R,I) .: {(c₃ * 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 - c₃ is Element of the carrier of R
- c₃ is Element of the carrier of R
B + (- c₃) is Element of the carrier of R
the addF of R . (B,(- c₃)) is Element of the carrier of R
(B - c₃) * x is Element of the carrier of R
the multF of R . ((B - c₃),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) - (c₃ * x) is Element of the carrier of R
- (c₃ * x) is Element of the carrier of R
(B * x) + (- (c₃ * x)) is Element of the carrier of R
the addF of R . ((B * x),(- (c₃ * 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 - c₃) * x) is Element of the carrier of R
the addF of R . ((B * (A - x)),((B - c₃) * 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)) - (c₃ * x) is Element of the carrier of R
(((B * A) - (B * x)) + (B * x)) + (- (c₃ * x)) is Element of the carrier of R
the addF of R . ((((B * A) - (B * x)) + (B * x)),(- (c₃ * x))) is Element of the carrier of R
(B * A) - (c₃ * x) is Element of the carrier of R
(B * A) + (- (c₃ * x)) is Element of the carrier of R
the addF of R . ((B * A),(- (c₃ * x))) is Element of the carrier of R
((B - c₃) * x) + (B * (A - x)) is Element of the carrier of R
the addF of R . (((B - c₃) * x),(B * (A - x))) 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
(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() 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
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 is Element of the carrier of (R,I)
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
I + J is Element of the carrier of (R,I)
the addF of (R,I) . (I,J) is Element of the carrier of (R,I)
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
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
J + I is Element of the carrier of (R,I)
the addF of (R,I) . (J,I) is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
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
J is Element of the carrier of (R,I)
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
B is Element of the carrier of (R,I)
J + B is Element of the carrier of (R,I)
the addF of (R,I) . (J,B) is Element of the carrier of (R,I)
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
y + Ab is Element of the carrier of R
the addF of R . (y,Ab) is Element of the carrier of R
Class ((R,I),(y + Ab)) is Element of K32( the carrier of R)
{(y + Ab)} is non empty set
(R,I) .: {(y + Ab)} is set
Aa - (y + Ab) is Element of the carrier of R
- (y + Ab) is Element of the carrier of R
Aa + (- (y + Ab)) is Element of the carrier of R
the addF of R . (Aa,(- (y + Ab))) is Element of the carrier of R
I + J is Element of the carrier of (R,I)
the addF of (R,I) . (I,J) is Element of the carrier of (R,I)
rd is Element of the carrier of R
Class ((R,I),rd) is Element of K32( the carrier of R)
{rd} is non empty set
(R,I) .: {rd} is set
A + y is Element of the carrier of R
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
rd - (A + y) is Element of the carrier of R
- (A + y) is Element of the carrier of R
rd + (- (A + y)) is Element of the carrier of R
the addF of R . (rd,(- (A + y))) is Element of the carrier of R
(rd - (A + y)) - (Aa - (y + Ab)) is Element of the carrier of R
- (Aa - (y + Ab)) is Element of the carrier of R
(rd - (A + y)) + (- (Aa - (y + Ab))) is Element of the carrier of R
the addF of R . ((rd - (A + y)),(- (Aa - (y + Ab)))) is Element of the carrier of R
(rd - (A + y)) - Aa is Element of the carrier of R
- Aa is Element of the carrier of R
(rd - (A + y)) + (- Aa) is Element of the carrier of R
the addF of R . ((rd - (A + y)),(- Aa)) is Element of the carrier of R
((rd - (A + y)) - Aa) + (y + Ab) is Element of the carrier of R
the addF of R . (((rd - (A + y)) - Aa),(y + Ab)) is Element of the carrier of R
(rd - (A + y)) + (y + Ab) is Element of the carrier of R
the addF of R . ((rd - (A + y)),(y + Ab)) is Element of the carrier of R
((rd - (A + y)) + (y + Ab)) - Aa is Element of the carrier of R
((rd - (A + y)) + (y + Ab)) + (- Aa) is Element of the carrier of R
the addF of R . (((rd - (A + y)) + (y + Ab)),(- Aa)) is Element of the carrier of R
rd - A is Element of the carrier of R
- A is Element of the carrier of R
rd + (- A) is Element of the carrier of R
the addF of R . (rd,(- A)) is Element of the carrier of R
(rd - A) - y is Element of the carrier of R
- y is Element of the carrier of R
(rd - A) + (- y) is Element of the carrier of R
the addF of R . ((rd - A),(- y)) is Element of the carrier of R
((rd - A) - y) + (y + Ab) is Element of the carrier of R
the addF of R . (((rd - A) - y),(y + Ab)) is Element of the carrier of R
(((rd - A) - y) + (y + Ab)) - Aa is Element of the carrier of R
(((rd - A) - y) + (y + Ab)) + (- Aa) is Element of the carrier of R
the addF of R . ((((rd - A) - y) + (y + Ab)),(- Aa)) is Element of the carrier of R
((rd - A) - y) + y is Element of the carrier of R
the addF of R . (((rd - A) - y),y) is Element of the carrier of R
(((rd - A) - y) + y) + Ab is Element of the carrier of R
the addF of R . ((((rd - A) - y) + y),Ab) is Element of the carrier of R
((((rd - A) - y) + y) + Ab) - Aa is Element of the carrier of R
((((rd - A) - y) + y) + Ab) + (- Aa) is Element of the carrier of R
the addF of R . (((((rd - A) - y) + y) + Ab),(- Aa)) is Element of the carrier of R
(rd - A) + Ab is Element of the carrier of R
the addF of R . ((rd - A),Ab) is Element of the carrier of R
((rd - A) + Ab) - Aa is Element of the carrier of R
((rd - A) + Ab) + (- Aa) is Element of the carrier of R
the addF of R . (((rd - A) + Ab),(- Aa)) is Element of the carrier of R
rd + Ab is Element of the carrier of R
the addF of R . (rd,Ab) is Element of the carrier of R
(rd + Ab) - A is Element of the carrier of R
(rd + Ab) + (- A) is Element of the carrier of R
the addF of R . ((rd + Ab),(- A)) is Element of the carrier of R
((rd + Ab) - A) - Aa is Element of the carrier of R
((rd + Ab) - A) + (- Aa) is Element of the carrier of R
the addF of R . (((rd + Ab) - A),(- 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
(rd + Ab) - (A + Aa) is Element of the carrier of R
- (A + Aa) is Element of the carrier of R
(rd + Ab) + (- (A + Aa)) is Element of the carrier of R
the addF of R . ((rd + Ab),(- (A + Aa))) is Element of the carrier of R
(I + J) + B is Element of the carrier of (R,I)
the addF of (R,I) . ((I + J),B) is Element of the carrier of (R,I)
Class ((R,I),(rd + Ab)) is Element of K32( the carrier of R)
{(rd + Ab)} is non empty set
(R,I) .: {(rd + Ab)} is set
Class ((R,I),(A + Aa)) is Element of K32( the carrier of R)
{(A + Aa)} is non empty set
(R,I) .: {(A + Aa)} is set
I + (J + B) is Element of the carrier of (R,I)
the addF of (R,I) . (I,(J + B)) is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
0. (R,I) is V71((R,I)) Element of the carrier of (R,I)
the ZeroF of (R,I) is Element of the carrier of (R,I)
the addF of (R,I) . (I,(0. (R,I))) is Element of the carrier of (R,I)
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
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 + B is Element of the carrier of R
the addF of R . (J,B) is Element of the carrier of R
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
0. R is V71(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
B - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
B + (- (0. R)) is Element of the carrier of R
the addF of R . (B,(- (0. R))) is Element of the carrier of R
(J + B) - J is Element of the carrier of R
- J is Element of the carrier of R
(J + B) + (- J) is Element of the carrier of R
the addF of R . ((J + B),(- J)) is Element of the carrier of R
J - J is Element of the carrier of R
J + (- J) is Element of the carrier of R
the addF of R . (J,(- J)) is Element of the carrier of R
(J - J) + B is Element of the carrier of R
the addF of R . ((J - J),B) is Element of the carrier of R
(0. R) + B is Element of the carrier of R
the addF of R . ((0. R),B) 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
I + (0. (R,I)) is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
the addF of (R,I) . (I,(0. (R,I))) is Element of the carrier of (R,I)
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
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 + B is Element of the carrier of R
the addF of R . (J,B) is Element of the carrier of R
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
- 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
A is Element of the carrier of (R,I)
I + A is Element of the carrier of (R,I)
the addF of (R,I) . (I,A) is Element of the carrier of (R,I)
J + (- J) is Element of the carrier of R
the addF of R . (J,(- J)) is Element of the carrier of R
Class ((R,I),(J + (- J))) is Element of K32( the carrier of R)
{(J + (- J))} is non empty set
(R,I) .: {(J + (- J))} is set
I is Element of the carrier of (R,I)
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
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)))
the multF of (R,I) . (I,J) is Element of the carrier of (R,I)
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
B is Element of the carrier of (R,I)
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
A * Ab 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 . (A,Ab) is Element of the carrier of R
Class ((R,I),(A * Ab)) is Element of K32( the carrier of R)
{(A * Ab)} is non empty set
(R,I) .: {(A * Ab)} is set
y - (A * Ab) is Element of the carrier of R
- (A * Ab) is Element of the carrier of R
y + (- (A * Ab)) is Element of the carrier of R
the addF of R . (y,(- (A * Ab))) is Element of the carrier of R
(y - (A * Ab)) * Aa is Element of the carrier of R
the multF of R . ((y - (A * Ab)),Aa) is Element of the carrier of R
J * B is Element of the carrier of (R,I)
the multF of (R,I) . (J,B) is Element of the carrier of (R,I)
rd is Element of the carrier of R
Class ((R,I),rd) is Element of K32( the carrier of R)
{rd} is non empty set
(R,I) .: {rd} is set
Ab * Aa is Element of the carrier of R
the multF of R . (Ab,Aa) is Element of the carrier of R
Class ((R,I),(Ab * Aa)) is Element of K32( the carrier of R)
{(Ab * Aa)} is non empty set
(R,I) .: {(Ab * Aa)} is set
rd - (Ab * Aa) is Element of the carrier of R
- (Ab * Aa) is Element of the carrier of R
rd + (- (Ab * Aa)) is Element of the carrier of R
the addF of R . (rd,(- (Ab * Aa))) is Element of the carrier of R
A * (rd - (Ab * Aa)) is Element of the carrier of R
the multF of R . (A,(rd - (Ab * Aa))) is Element of the carrier of R
y * Aa is Element of the carrier of R
the multF of R . (y,Aa) is Element of the carrier of R
(A * Ab) * Aa is Element of the carrier of R
the multF of R . ((A * Ab),Aa) is Element of the carrier of R
(y * Aa) - ((A * Ab) * Aa) is Element of the carrier of R
- ((A * Ab) * Aa) is Element of the carrier of R
(y * Aa) + (- ((A * Ab) * Aa)) is Element of the carrier of R
the addF of R . ((y * Aa),(- ((A * Ab) * Aa))) is Element of the carrier of R
A * rd is Element of the carrier of R
the multF of R . (A,rd) is Element of the carrier of R
A * (Ab * Aa) is Element of the carrier of R
the multF of R . (A,(Ab * Aa)) is Element of the carrier of R
(A * rd) - (A * (Ab * Aa)) is Element of the carrier of R
- (A * (Ab * Aa)) is Element of the carrier of R
(A * rd) + (- (A * (Ab * Aa))) is Element of the carrier of R
the addF of R . ((A * rd),(- (A * (Ab * Aa)))) is Element of the carrier of R
(A * rd) - ((A * Ab) * Aa) is Element of the carrier of R
(A * rd) + (- ((A * Ab) * Aa)) is Element of the carrier of R
the addF of R . ((A * rd),(- ((A * Ab) * Aa))) is Element of the carrier of R
((y * Aa) - ((A * Ab) * Aa)) - ((A * rd) - ((A * Ab) * Aa)) is Element of the carrier of R
- ((A * rd) - ((A * Ab) * Aa)) is Element of the carrier of R
((y * Aa) - ((A * Ab) * Aa)) + (- ((A * rd) - ((A * Ab) * Aa))) is Element of the carrier of R
the addF of R . (((y * Aa) - ((A * Ab) * Aa)),(- ((A * rd) - ((A * Ab) * Aa)))) is Element of the carrier of R
(y * Aa) - (A * rd) is Element of the carrier of R
- (A * rd) is Element of the carrier of R
(y * Aa) + (- (A * rd)) is Element of the carrier of R
the addF of R . ((y * Aa),(- (A * rd))) is Element of the carrier of R
(I * J) * B is Element of the carrier of (R,I)
the multF of (R,I) . ((I * J),B) is Element of the carrier of (R,I)
Class ((R,I),(y * Aa)) is Element of K32( the carrier of R)
{(y * Aa)} is non empty set
(R,I) .: {(y * Aa)} is set
Class ((R,I),(A * rd)) is Element of K32( the carrier of R)
{(A * rd)} is non empty set
(R,I) .: {(A * rd)} is set
I * (J * B) is Element of the carrier of (R,I)
the multF of (R,I) . (I,(J * B)) is Element of the carrier of (R,I)
1. R is Element of the carrier of R
the OneF of R is Element of the carrier of R
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
1. (R,I) is Element of the carrier of (R,I)
the OneF of (R,I) is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
I * (1. (R,I)) is Element of the carrier of (R,I)
the multF of (R,I) . (I,(1. (R,I))) is Element of the carrier of (R,I)
J is Element of the carrier of (R,I)
(1. (R,I)) * J is Element of the carrier of (R,I)
the multF of (R,I) . ((1. (R,I)),J) is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
J is Element of the carrier of (R,I)
B is Element of the carrier of (R,I)
J + B is Element of the carrier of (R,I)
the addF of (R,I) . (J,B) is Element of the carrier of (R,I)
I * (J + B) is Element of the carrier of (R,I)
the multF of (R,I) . (I,(J + B)) is Element of the carrier of (R,I)
I * J is Element of the carrier of (R,I)
the multF of (R,I) . (I,J) is Element of the carrier of (R,I)
I * B is Element of the carrier of (R,I)
the multF of (R,I) . (I,B) is Element of the carrier of (R,I)
(I * J) + (I * B) is Element of the carrier of (R,I)
the addF of (R,I) . ((I * J),(I * B)) is Element of the carrier of (R,I)
(J + B) * I is Element of the carrier of (R,I)
the multF of (R,I) . ((J + B),I) is Element of the carrier of (R,I)
J * I is Element of the carrier of (R,I)
the multF of (R,I) . (J,I) is Element of the carrier of (R,I)
B * I is Element of the carrier of (R,I)
the multF of (R,I) . (B,I) is Element of the carrier of (R,I)
(J * I) + (B * I) is Element of the carrier of (R,I)
the addF of (R,I) . ((J * I),(B * I)) is Element of the carrier of (R,I)
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
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
Ab * A is Element of the carrier of R
the multF of R . (Ab,A) is Element of the carrier of R
Class ((R,I),(Ab * A)) is Element of K32( the carrier of R)
{(Ab * A)} is non empty set
(R,I) .: {(Ab * A)} is set
(Ab * A) - Aa is Element of the carrier of R
- Aa is Element of the carrier of R
(Ab * A) + (- Aa) is Element of the carrier of R
the addF of R . ((Ab * A),(- Aa)) is Element of the carrier of R
rd is Element of the carrier of R
Class ((R,I),rd) is Element of K32( the carrier of R)
{rd} is non empty set
(R,I) .: {rd} is set
A * rd is Element of the carrier of R
the multF of R . (A,rd) is Element of the carrier of R
Class ((R,I),(A * rd)) is Element of K32( the carrier of R)
{(A * rd)} is non empty set
(R,I) .: {(A * rd)} is set
y - (A * rd) is Element of the carrier of R
- (A * rd) is Element of the carrier of R
y + (- (A * rd)) is Element of the carrier of R
the addF of R . (y,(- (A * rd))) is Element of the carrier of R
sd is Element of the carrier of R
Class ((R,I),sd) is Element of K32( the carrier of R)
{sd} is non empty set
(R,I) .: {sd} is set
A * Ab is Element of the carrier of R
the multF of R . (A,Ab) is Element of the carrier of R
Class ((R,I),(A * Ab)) is Element of K32( the carrier of R)
{(A * Ab)} is non empty set
(R,I) .: {(A * Ab)} is set
sd - (A * Ab) is Element of the carrier of R
- (A * Ab) is Element of the carrier of R
sd + (- (A * Ab)) is Element of the carrier of R
the addF of R . (sd,(- (A * Ab))) is Element of the carrier of R
bc is Element of the carrier of R
Class ((R,I),bc) is Element of K32( the carrier of R)
{bc} is non empty set
(R,I) .: {bc} is set
rd + Ab is Element of the carrier of R
the addF of R . (rd,Ab) is Element of the carrier of R
Class ((R,I),(rd + Ab)) is Element of K32( the carrier of R)
{(rd + Ab)} is non empty set
(R,I) .: {(rd + Ab)} is set
bc - (rd + Ab) is Element of the carrier of R
- (rd + Ab) is Element of the carrier of R
bc + (- (rd + Ab)) is Element of the carrier of R
the addF of R . (bc,(- (rd + Ab))) is Element of the carrier of R
(bc - (rd + Ab)) * A is Element of the carrier of R
the multF of R . ((bc - (rd + Ab)),A) is Element of the carrier of R
A * (bc - (rd + Ab)) is Element of the carrier of R
the multF of R . (A,(bc - (rd + Ab))) is Element of the carrier of R
(A * (bc - (rd + Ab))) - (y - (A * rd)) is Element of the carrier of R
- (y - (A * rd)) is Element of the carrier of R
(A * (bc - (rd + Ab))) + (- (y - (A * rd))) is Element of the carrier of R
the addF of R . ((A * (bc - (rd + Ab))),(- (y - (A * rd)))) is Element of the carrier of R
((A * (bc - (rd + Ab))) - (y - (A * rd))) - (sd - (A * Ab)) is Element of the carrier of R
- (sd - (A * Ab)) is Element of the carrier of R
((A * (bc - (rd + Ab))) - (y - (A * rd))) + (- (sd - (A * Ab))) is Element of the carrier of R
the addF of R . (((A * (bc - (rd + Ab))) - (y - (A * rd))),(- (sd - (A * Ab)))) is Element of the carrier of R
A * bc is Element of the carrier of R
the multF of R . (A,bc) is Element of the carrier of R
A * (rd + Ab) is Element of the carrier of R
the multF of R . (A,(rd + Ab)) is Element of the carrier of R
(A * bc) - (A * (rd + Ab)) is Element of the carrier of R
- (A * (rd + Ab)) is Element of the carrier of R
(A * bc) + (- (A * (rd + Ab))) is Element of the carrier of R
the addF of R . ((A * bc),(- (A * (rd + Ab)))) is Element of the carrier of R
((A * bc) - (A * (rd + Ab))) - (y - (A * rd)) is Element of the carrier of R
((A * bc) - (A * (rd + Ab))) + (- (y - (A * rd))) is Element of the carrier of R
the addF of R . (((A * bc) - (A * (rd + Ab))),(- (y - (A * rd)))) is Element of the carrier of R
(((A * bc) - (A * (rd + Ab))) - (y - (A * rd))) - (sd - (A * Ab)) is Element of the carrier of R
(((A * bc) - (A * (rd + Ab))) - (y - (A * rd))) + (- (sd - (A * Ab))) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * (rd + Ab))) - (y - (A * rd))),(- (sd - (A * Ab)))) is Element of the carrier of R
(A * rd) + (A * Ab) is Element of the carrier of R
the addF of R . ((A * rd),(A * Ab)) is Element of the carrier of R
(A * bc) - ((A * rd) + (A * Ab)) is Element of the carrier of R
- ((A * rd) + (A * Ab)) is Element of the carrier of R
(A * bc) + (- ((A * rd) + (A * Ab))) is Element of the carrier of R
the addF of R . ((A * bc),(- ((A * rd) + (A * Ab)))) is Element of the carrier of R
((A * bc) - ((A * rd) + (A * Ab))) - (y - (A * rd)) is Element of the carrier of R
((A * bc) - ((A * rd) + (A * Ab))) + (- (y - (A * rd))) is Element of the carrier of R
the addF of R . (((A * bc) - ((A * rd) + (A * Ab))),(- (y - (A * rd)))) is Element of the carrier of R
(((A * bc) - ((A * rd) + (A * Ab))) - (y - (A * rd))) - (sd - (A * Ab)) is Element of the carrier of R
(((A * bc) - ((A * rd) + (A * Ab))) - (y - (A * rd))) + (- (sd - (A * Ab))) is Element of the carrier of R
the addF of R . ((((A * bc) - ((A * rd) + (A * Ab))) - (y - (A * rd))),(- (sd - (A * Ab)))) is Element of the carrier of R
(A * bc) - (A * rd) is Element of the carrier of R
(A * bc) + (- (A * rd)) is Element of the carrier of R
the addF of R . ((A * bc),(- (A * rd))) is Element of the carrier of R
((A * bc) - (A * rd)) - (A * Ab) is Element of the carrier of R
((A * bc) - (A * rd)) + (- (A * Ab)) is Element of the carrier of R
the addF of R . (((A * bc) - (A * rd)),(- (A * Ab))) is Element of the carrier of R
(((A * bc) - (A * rd)) - (A * Ab)) - (y - (A * rd)) is Element of the carrier of R
(((A * bc) - (A * rd)) - (A * Ab)) + (- (y - (A * rd))) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * rd)) - (A * Ab)),(- (y - (A * rd)))) is Element of the carrier of R
((((A * bc) - (A * rd)) - (A * Ab)) - (y - (A * rd))) - (sd - (A * Ab)) is Element of the carrier of R
((((A * bc) - (A * rd)) - (A * Ab)) - (y - (A * rd))) + (- (sd - (A * Ab))) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * rd)) - (A * Ab)) - (y - (A * rd))),(- (sd - (A * Ab)))) is Element of the carrier of R
(((A * bc) - (A * rd)) - (A * Ab)) - y is Element of the carrier of R
- y is Element of the carrier of R
(((A * bc) - (A * rd)) - (A * Ab)) + (- y) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * rd)) - (A * Ab)),(- y)) is Element of the carrier of R
((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * rd)) - (A * Ab)) - y),(A * rd)) is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) - (sd - (A * Ab)) is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) + (- (sd - (A * Ab))) is Element of the carrier of R
the addF of R . ((((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)),(- (sd - (A * Ab)))) is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) - sd is Element of the carrier of R
- sd is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) + (- sd) is Element of the carrier of R
the addF of R . ((((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)),(- sd)) is Element of the carrier of R
((((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) - sd) + (A * Ab) is Element of the carrier of R
the addF of R . (((((((A * bc) - (A * rd)) - (A * Ab)) - y) + (A * rd)) - sd),(A * Ab)) is Element of the carrier of R
(((A * bc) - (A * rd)) - (A * Ab)) + (A * rd) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * rd)) - (A * Ab)),(A * rd)) is Element of the carrier of R
((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y is Element of the carrier of R
((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) + (- y) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)),(- y)) is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y) - sd is Element of the carrier of R
(((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y) + (- sd) is Element of the carrier of R
the addF of R . ((((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y),(- sd)) is Element of the carrier of R
((((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y) - sd) + (A * Ab) is Element of the carrier of R
the addF of R . (((((((A * bc) - (A * rd)) - (A * Ab)) + (A * rd)) - y) - sd),(A * Ab)) is Element of the carrier of R
((A * bc) - (A * rd)) + (A * rd) is Element of the carrier of R
the addF of R . (((A * bc) - (A * rd)),(A * rd)) is Element of the carrier of R
(((A * bc) - (A * rd)) + (A * rd)) - (A * Ab) is Element of the carrier of R
(((A * bc) - (A * rd)) + (A * rd)) + (- (A * Ab)) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * rd)) + (A * rd)),(- (A * Ab))) is Element of the carrier of R
((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y is Element of the carrier of R
((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) + (- y) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)),(- y)) is Element of the carrier of R
(((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y) - sd is Element of the carrier of R
(((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y) + (- sd) is Element of the carrier of R
the addF of R . ((((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y),(- sd)) is Element of the carrier of R
((((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y) - sd) + (A * Ab) is Element of the carrier of R
the addF of R . (((((((A * bc) - (A * rd)) + (A * rd)) - (A * Ab)) - y) - sd),(A * Ab)) is Element of the carrier of R
(A * bc) - (A * Ab) is Element of the carrier of R
(A * bc) + (- (A * Ab)) is Element of the carrier of R
the addF of R . ((A * bc),(- (A * Ab))) is Element of the carrier of R
((A * bc) - (A * Ab)) - y is Element of the carrier of R
((A * bc) - (A * Ab)) + (- y) is Element of the carrier of R
the addF of R . (((A * bc) - (A * Ab)),(- y)) is Element of the carrier of R
(((A * bc) - (A * Ab)) - y) - sd is Element of the carrier of R
(((A * bc) - (A * Ab)) - y) + (- sd) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * Ab)) - y),(- sd)) is Element of the carrier of R
((((A * bc) - (A * Ab)) - y) - sd) + (A * Ab) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * Ab)) - y) - sd),(A * Ab)) is Element of the carrier of R
(((A * bc) - (A * Ab)) - y) + (A * Ab) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * Ab)) - y),(A * Ab)) is Element of the carrier of R
((((A * bc) - (A * Ab)) - y) + (A * Ab)) - sd is Element of the carrier of R
((((A * bc) - (A * Ab)) - y) + (A * Ab)) + (- sd) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * Ab)) - y) + (A * Ab)),(- sd)) is Element of the carrier of R
((A * bc) - (A * Ab)) + (A * Ab) is Element of the carrier of R
the addF of R . (((A * bc) - (A * Ab)),(A * Ab)) is Element of the carrier of R
(((A * bc) - (A * Ab)) + (A * Ab)) - y is Element of the carrier of R
(((A * bc) - (A * Ab)) + (A * Ab)) + (- y) is Element of the carrier of R
the addF of R . ((((A * bc) - (A * Ab)) + (A * Ab)),(- y)) is Element of the carrier of R
((((A * bc) - (A * Ab)) + (A * Ab)) - y) - sd is Element of the carrier of R
((((A * bc) - (A * Ab)) + (A * Ab)) - y) + (- sd) is Element of the carrier of R
the addF of R . (((((A * bc) - (A * Ab)) + (A * Ab)) - y),(- sd)) is Element of the carrier of R
(A * bc) - y is Element of the carrier of R
(A * bc) + (- y) is Element of the carrier of R
the addF of R . ((A * bc),(- y)) is Element of the carrier of R
((A * bc) - y) - sd is Element of the carrier of R
((A * bc) - y) + (- sd) is Element of the carrier of R
the addF of R . (((A * bc) - y),(- sd)) is Element of the carrier of R
y + sd is Element of the carrier of R
the addF of R . (y,sd) is Element of the carrier of R
(A * bc) - (y + sd) is Element of the carrier of R
- (y + sd) is Element of the carrier of R
(A * bc) + (- (y + sd)) is Element of the carrier of R
the addF of R . ((A * bc),(- (y + sd))) is Element of the carrier of R
Class ((R,I),(A * bc)) is Element of K32( the carrier of R)
{(A * bc)} is non empty set
(R,I) .: {(A * bc)} is set
Class ((R,I),(y + sd)) is Element of K32( the carrier of R)
{(y + sd)} is non empty set
(R,I) .: {(y + sd)} is set
ba is Element of the carrier of R
Class ((R,I),ba) is Element of K32( the carrier of R)
{ba} is non empty set
(R,I) .: {ba} is set
rd * A is Element of the carrier of R
the multF of R . (rd,A) is Element of the carrier of R
Class ((R,I),(rd * A)) is Element of K32( the carrier of R)
{(rd * A)} is non empty set
(R,I) .: {(rd * A)} is set
(rd * A) - ba is Element of the carrier of R
- ba is Element of the carrier of R
(rd * A) + (- ba) is Element of the carrier of R
the addF of R . ((rd * A),(- ba)) is Element of the carrier of R
((bc - (rd + Ab)) * A) + ((rd * A) - ba) is Element of the carrier of R
the addF of R . (((bc - (rd + Ab)) * A),((rd * A) - ba)) is Element of the carrier of R
(((bc - (rd + Ab)) * A) + ((rd * A) - ba)) + ((Ab * A) - Aa) is Element of the carrier of R
the addF of R . ((((bc - (rd + Ab)) * A) + ((rd * A) - ba)),((Ab * A) - Aa)) is Element of the carrier of R
bc * A is Element of the carrier of R
the multF of R . (bc,A) is Element of the carrier of R
(rd + Ab) * A is Element of the carrier of R
the multF of R . ((rd + Ab),A) is Element of the carrier of R
(bc * A) - ((rd + Ab) * A) is Element of the carrier of R
- ((rd + Ab) * A) is Element of the carrier of R
(bc * A) + (- ((rd + Ab) * A)) is Element of the carrier of R
the addF of R . ((bc * A),(- ((rd + Ab) * A))) is Element of the carrier of R
((bc * A) - ((rd + Ab) * A)) + ((rd * A) - ba) is Element of the carrier of R
the addF of R . (((bc * A) - ((rd + Ab) * A)),((rd * A) - ba)) is Element of the carrier of R
(((bc * A) - ((rd + Ab) * A)) + ((rd * A) - ba)) + ((Ab * A) - Aa) is Element of the carrier of R
the addF of R . ((((bc * A) - ((rd + Ab) * A)) + ((rd * A) - ba)),((Ab * A) - Aa)) is Element of the carrier of R
(rd * A) + (Ab * A) is Element of the carrier of R
the addF of R . ((rd * A),(Ab * A)) is Element of the carrier of R
(bc * A) - ((rd * A) + (Ab * A)) is Element of the carrier of R
- ((rd * A) + (Ab * A)) is Element of the carrier of R
(bc * A) + (- ((rd * A) + (Ab * A))) is Element of the carrier of R
the addF of R . ((bc * A),(- ((rd * A) + (Ab * A)))) is Element of the carrier of R
((bc * A) - ((rd * A) + (Ab * A))) + ((rd * A) - ba) is Element of the carrier of R
the addF of R . (((bc * A) - ((rd * A) + (Ab * A))),((rd * A) - ba)) is Element of the carrier of R
(((bc * A) - ((rd * A) + (Ab * A))) + ((rd * A) - ba)) + ((Ab * A) - Aa) is Element of the carrier of R
the addF of R . ((((bc * A) - ((rd * A) + (Ab * A))) + ((rd * A) - ba)),((Ab * A) - Aa)) is Element of the carrier of R
(bc * A) - (rd * A) is Element of the carrier of R
- (rd * A) is Element of the carrier of R
(bc * A) + (- (rd * A)) is Element of the carrier of R
the addF of R . ((bc * A),(- (rd * A))) is Element of the carrier of R
((bc * A) - (rd * A)) - (Ab * A) is Element of the carrier of R
- (Ab * A) is Element of the carrier of R
((bc * A) - (rd * A)) + (- (Ab * A)) is Element of the carrier of R
the addF of R . (((bc * A) - (rd * A)),(- (Ab * A))) is Element of the carrier of R
(((bc * A) - (rd * A)) - (Ab * A)) + ((rd * A) - ba) is Element of the carrier of R
the addF of R . ((((bc * A) - (rd * A)) - (Ab * A)),((rd * A) - ba)) is Element of the carrier of R
((((bc * A) - (rd * A)) - (Ab * A)) + ((rd * A) - ba)) + ((Ab * A) - Aa) is Element of the carrier of R
the addF of R . (((((bc * A) - (rd * A)) - (Ab * A)) + ((rd * A) - ba)),((Ab * A) - Aa)) is Element of the carrier of R
(((bc * A) - (rd * A)) - (Ab * A)) + (rd * A) is Element of the carrier of R
the addF of R . ((((bc * A) - (rd * A)) - (Ab * A)),(rd * A)) is Element of the carrier of R
((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba is Element of the carrier of R
((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) + (- ba) is Element of the carrier of R
the addF of R . (((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)),(- ba)) is Element of the carrier of R
(((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba) + ((Ab * A) - Aa) is Element of the carrier of R
the addF of R . ((((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba),((Ab * A) - Aa)) is Element of the carrier of R
(((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba) + (Ab * A) is Element of the carrier of R
the addF of R . ((((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba),(Ab * A)) is Element of the carrier of R
((((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba) + (Ab * A)) - Aa is Element of the carrier of R
((((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba) + (Ab * A)) + (- Aa) is Element of the carrier of R
the addF of R . (((((((bc * A) - (rd * A)) - (Ab * A)) + (rd * A)) - ba) + (Ab * A)),(- Aa)) is Element of the carrier of R
((bc * A) - (rd * A)) + (rd * A) is Element of the carrier of R
the addF of R . (((bc * A) - (rd * A)),(rd * A)) is Element of the carrier of R
(((bc * A) - (rd * A)) + (rd * A)) - (Ab * A) is Element of the carrier of R
(((bc * A) - (rd * A)) + (rd * A)) + (- (Ab * A)) is Element of the carrier of R
the addF of R . ((((bc * A) - (rd * A)) + (rd * A)),(- (Ab * A))) is Element of the carrier of R
((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba is Element of the carrier of R
((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) + (- ba) is Element of the carrier of R
the addF of R . (((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)),(- ba)) is Element of the carrier of R
(((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba) + (Ab * A) is Element of the carrier of R
the addF of R . ((((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba),(Ab * A)) is Element of the carrier of R
((((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba) + (Ab * A)) - Aa is Element of the carrier of R
((((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba) + (Ab * A)) + (- Aa) is Element of the carrier of R
the addF of R . (((((((bc * A) - (rd * A)) + (rd * A)) - (Ab * A)) - ba) + (Ab * A)),(- Aa)) is Element of the carrier of R
(bc * A) - (Ab * A) is Element of the carrier of R
(bc * A) + (- (Ab * A)) is Element of the carrier of R
the addF of R . ((bc * A),(- (Ab * A))) is Element of the carrier of R
((bc * A) - (Ab * A)) - ba is Element of the carrier of R
((bc * A) - (Ab * A)) + (- ba) is Element of the carrier of R
the addF of R . (((bc * A) - (Ab * A)),(- ba)) is Element of the carrier of R
(((bc * A) - (Ab * A)) - ba) + (Ab * A) is Element of the carrier of R
the addF of R . ((((bc * A) - (Ab * A)) - ba),(Ab * A)) is Element of the carrier of R
((((bc * A) - (Ab * A)) - ba) + (Ab * A)) - Aa is Element of the carrier of R
((((bc * A) - (Ab * A)) - ba) + (Ab * A)) + (- Aa) is Element of the carrier of R
the addF of R . (((((bc * A) - (Ab * A)) - ba) + (Ab * A)),(- Aa)) is Element of the carrier of R
((bc * A) - (Ab * A)) + (Ab * A) is Element of the carrier of R
the addF of R . (((bc * A) - (Ab * A)),(Ab * A)) is Element of the carrier of R
(((bc * A) - (Ab * A)) + (Ab * A)) - ba is Element of the carrier of R
(((bc * A) - (Ab * A)) + (Ab * A)) + (- ba) is Element of the carrier of R
the addF of R . ((((bc * A) - (Ab * A)) + (Ab * A)),(- ba)) is Element of the carrier of R
((((bc * A) - (Ab * A)) + (Ab * A)) - ba) - Aa is Element of the carrier of R
((((bc * A) - (Ab * A)) + (Ab * A)) - ba) + (- Aa) is Element of the carrier of R
the addF of R . (((((bc * A) - (Ab * A)) + (Ab * A)) - ba),(- Aa)) is Element of the carrier of R
(bc * A) - ba is Element of the carrier of R
(bc * A) + (- ba) is Element of the carrier of R
the addF of R . ((bc * A),(- ba)) is Element of the carrier of R
((bc * A) - ba) - Aa is Element of the carrier of R
((bc * A) - ba) + (- Aa) is Element of the carrier of R
the addF of R . (((bc * A) - ba),(- Aa)) is Element of the carrier of R
ba + Aa is Element of the carrier of R
the addF of R . (ba,Aa) is Element of the carrier of R
(bc * A) - (ba + Aa) is Element of the carrier of R
- (ba + Aa) is Element of the carrier of R
(bc * A) + (- (ba + Aa)) is Element of the carrier of R
the addF of R . ((bc * A),(- (ba + Aa))) is Element of the carrier of R
Class ((R,I),(bc * A)) is Element of K32( the carrier of R)
{(bc * A)} is non empty set
(R,I) .: {(bc * A)} is set
Class ((R,I),(ba + Aa)) is Element of K32( the carrier of R)
{(ba + Aa)} is non empty set
(R,I) .: {(ba + Aa)} is set
R is non empty 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 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 left_add-cancelable right_add-cancelable right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
(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
the carrier of (R,I) is non empty set
x is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
x * I 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) . (x,I) is Element of the carrier of (R,I)
I * x is Element of the carrier of (R,I)
the multF of (R,I) . (I,x) is Element of the carrier of (R,I)
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
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 * 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))
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 . (J,B) is Element of the carrier of R
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 non empty left_add-cancelable right_add-cancelable right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
(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
0. R is V71(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
(1. R) - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
(1. R) + (- (0. 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 . ((1. R),(- (0. R))) is Element of the carrier of R
0. (R,I) is V71((R,I)) Element of the carrier of (R,I)
the carrier of (R,I) is non empty set
the ZeroF of (R,I) is Element of the carrier of (R,I)
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,I) is Element of the carrier of (R,I)
the OneF of (R,I) is Element of the carrier of (R,I)
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 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 left_add-cancelable right_add-cancelable right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
(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
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
0. (R,I) is V71((R,I)) Element of the carrier of (R,I)
the carrier of (R,I) is non empty set
the ZeroF of (R,I) is Element of the carrier of (R,I)
x is Element of the carrier of (R,I)
I is Element of the carrier of (R,I)
x * I 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) . (x,I) is Element of the carrier of (R,I)
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
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 * 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))
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 . (J,B) is Element of the carrier of R
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
(J * B) - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
(J * B) + (- (0. 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))
the addF of R . ((J * B),(- (0. R))) is Element of the carrier of R
J - (0. R) is Element of the carrier of R
J + (- (0. R)) is Element of the carrier of R
the addF of R . (J,(- (0. R))) is Element of the carrier of R
B - (0. R) is Element of the carrier of R
B + (- (0. R)) is Element of the carrier of R
the addF of R . (B,(- (0. R))) is Element of 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 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 . (x,I) 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
Class ((R,I),I) is Element of K32( the carrier of R)
{I} is non empty set
(R,I) .: {I} is set
(x * I) - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
(x * I) + (- (0. 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))
the addF of R . ((x * I),(- (0. R))) is Element of the carrier of R
Class ((R,I),(x * I)) is Element of K32( the carrier of R)
{(x * I)} is non empty set
(R,I) .: {(x * I)} is set
J is Element of the carrier of (R,I)
B is Element of the carrier of (R,I)
J * B 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) . (J,B) is Element of the carrier of (R,I)
x - (0. R) is Element of the carrier of R
x + (- (0. R)) is Element of the carrier of R
the addF of R . (x,(- (0. R))) is Element of the carrier of R
I - (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
R is non empty 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 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 left_add-cancelable right_add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
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 left_add-cancelable right_add-cancelable right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
(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
the carrier of (R,I) is non empty set
x is Element of the carrier of (R,I)
0. (R,I) is V71((R,I)) Element of the carrier of (R,I)
the ZeroF of (R,I) is Element of the carrier of (R,I)
I is Element of the carrier of R
Class ((R,I),I) is Element of K32( the carrier of R)
{I} is non empty set
(R,I) .: {I} is set
{ ((I * b₁) + b₂) where b₁, b₂ is Element of the carrier of R : b₂ in I } is set
B is set
A is Element of the carrier of R
I * A 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 . (I,A) is Element of the carrier of R
y is Element of the carrier of R
(I * 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))
the addF of R . ((I * A),y) 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
B is Element of K32( the carrier of R)
y is Element of the carrier of R
A is Element of the carrier of R
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
Aa is Element of the carrier of R
I * Aa is Element of the carrier of R
the multF of R . (I,Aa) is Element of the carrier of R
Ab is Element of the carrier of R
(I * Aa) + 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 . ((I * Aa),Ab) is Element of the carrier of R
A * Ab is Element of the carrier of R
the multF of R . (A,Ab) is Element of the carrier of R
Aa * A is Element of the carrier of R
the multF of R . (Aa,A) is Element of the carrier of R
I * (Aa * A) is Element of the carrier of R
the multF of R . (I,(Aa * A)) is Element of the carrier of R
(I * (Aa * A)) + (A * Ab) is Element of the carrier of R
the addF of R . ((I * (Aa * A)),(A * Ab)) is Element of the carrier of R
(I * Aa) * A is Element of the carrier of R
the multF of R . ((I * Aa),A) is Element of the carrier of R
((I * Aa) * A) + (A * Ab) is Element of the carrier of R
the addF of R . (((I * Aa) * A),(A * Ab)) is Element of the carrier of R
Ab * A is Element of the carrier of R
the multF of R . (Ab,A) is Element of the carrier of R
((I * Aa) * A) + (Ab * A) is Element of the carrier of R
the addF of R . (((I * Aa) * A),(Ab * A)) is Element of the carrier of R
y * A is Element of the carrier of R
the multF of R . (y,A) is Element of the carrier of R
A is set
I * (0. R) 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 . (I,(0. R)) is Element of the carrier of R
y is Element of I
(I * (0. R)) + 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))
the addF of R . ((I * (0. R)),y) is Element of the carrier of R
(0. R) + y is Element of the carrier of R
the addF of R . ((0. R),y) is Element of the carrier of R
y is Element of the carrier of R
A is Element of the carrier of R
y * A 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 . (y,A) is Element of the carrier of R
Aa is Element of the carrier of R
I * Aa is Element of the carrier of R
the multF of R . (I,Aa) is Element of the carrier of R
Ab is Element of the carrier of R
(I * Aa) + 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 . ((I * Aa),Ab) is Element of the carrier of R
A * Ab is Element of the carrier of R
the multF of R . (A,Ab) is Element of the carrier of R
Aa * A is Element of the carrier of R
the multF of R . (Aa,A) is Element of the carrier of R
I * (Aa * A) is Element of the carrier of R
the multF of R . (I,(Aa * A)) is Element of the carrier of R
(I * (Aa * A)) + (A * Ab) is Element of the carrier of R
the addF of R . ((I * (Aa * A)),(A * Ab)) is Element of the carrier of R
(I * Aa) * A is Element of the carrier of R
the multF of R . ((I * Aa),A) is Element of the carrier of R
((I * Aa) * A) + (A * Ab) is Element of the carrier of R
the addF of R . (((I * Aa) * A),(A * Ab)) is Element of the carrier of R
Ab * A is Element of the carrier of R
the multF of R . (Ab,A) is Element of the carrier of R
((I * Aa) * A) + (Ab * A) is Element of the carrier of R
the addF of R . (((I * Aa) * A),(Ab * A)) 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
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
Aa is Element of the carrier of R
I * Aa 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 . (I,Aa) is Element of the carrier of R
Ab is Element of the carrier of R
(I * Aa) + Ab is Element of the carrier of R
the addF of R . ((I * Aa),Ab) is Element of the carrier of R
rd is Element of the carrier of R
I * rd is Element of the carrier of R
the multF of R . (I,rd) is Element of the carrier of R
sd is Element of the carrier of R
(I * rd) + sd is Element of the carrier of R
the addF of R . ((I * rd),sd) is Element of the carrier of R
Aa + rd is Element of the carrier of R
the addF of R . (Aa,rd) is Element of the carrier of R
I * (Aa + rd) is Element of the carrier of R
the multF of R . (I,(Aa + rd)) is Element of the carrier of R
Ab + sd is Element of the carrier of R
the addF of R . (Ab,sd) is Element of the carrier of R
(I * (Aa + rd)) + (Ab + sd) is Element of the carrier of R
the addF of R . ((I * (Aa + rd)),(Ab + sd)) is Element of the carrier of R
(I * Aa) + (I * rd) is Element of the carrier of R
the addF of R . ((I * Aa),(I * rd)) is Element of the carrier of R
((I * Aa) + (I * rd)) + (Ab + sd) is Element of the carrier of R
the addF of R . (((I * Aa) + (I * rd)),(Ab + sd)) is Element of the carrier of R
((I * Aa) + (I * rd)) + Ab is Element of the carrier of R
the addF of R . (((I * Aa) + (I * rd)),Ab) is Element of the carrier of R
(((I * Aa) + (I * rd)) + Ab) + sd is Element of the carrier of R
the addF of R . ((((I * Aa) + (I * rd)) + Ab),sd) is Element of the carrier of R
((I * Aa) + Ab) + (I * rd) is Element of the carrier of R
the addF of R . (((I * Aa) + Ab),(I * rd)) is Element of the carrier of R
(((I * Aa) + Ab) + (I * rd)) + sd is Element of the carrier of R
the addF of R . ((((I * Aa) + Ab) + (I * rd)),sd) is Element of the carrier of R
A + y 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 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,(- (0. 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
the OneF of R is Element of the carrier of R
I * (1. R) 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 . (I,(1. R)) is Element of the carrier of R
(I * (1. R)) + (0. R) is Element of the carrier of R
the addF of R . ((I * (1. 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
A is Element of the carrier of R
I * A is Element of the carrier of R
the multF of R . (I,A) is Element of the carrier of R
y is Element of the carrier of R
(I * A) + y is Element of the carrier of R
the addF of R . ((I * A),y) is Element of the carrier of R
(1. R) - (I * A) is Element of the carrier of R
- (I * A) is Element of the carrier of R
(1. R) + (- (I * A)) is Element of the carrier of R
the addF of R . ((1. R),(- (I * 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
Aa is Element of the carrier of (R,I)
Aa * 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) . (Aa,x) is Element of the carrier of (R,I)
1. (R,I) is Element of the carrier of (R,I)
the OneF of (R,I) is Element of the carrier of (R,I)
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
A * I is Element of the carrier of R
the multF of R . (A,I) is Element of the carrier of R
Class ((R,I),(A * I)) is Element of K32( the carrier of R)
{(A * I)} is non empty set
(R,I) .: {(A * I)} is set
Class ((R,I),(I * A)) is Element of K32( the carrier of R)
{(I * A)} is non empty set
(R,I) .: {(I * A)} 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 non empty left_add-cancelable right_add-cancelable right_complementable strict unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
(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
x is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
I is set
the carrier of (R,I) is non empty 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
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
0. (R,I) is V71((R,I)) Element of the carrier of (R,I)
the ZeroF of (R,I) is Element of the carrier of (R,I)
B is Element of the carrier of (R,I)
J - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
J + (- (0. 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,(- (0. R))) is Element of the carrier of R
1. (R,I) is Element of the carrier of (R,I)
the OneF of (R,I) is Element of the carrier of (R,I)
A is Element of the carrier of (R,I)
A * B 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) . (A,B) is Element of the carrier of (R,I)
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
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
y * J 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 . (y,J) is Element of the carrier of R
Class ((R,I),(y * J)) is Element of K32( the carrier of R)
{(y * J)} is non empty set
(R,I) .: {(y * J)} is set
(y * J) - (1. R) is Element of the carrier of R
- (1. R) is Element of the carrier of R
(y * J) + (- (1. R)) is Element of the carrier of R
the addF of R . ((y * J),(- (1. R))) is Element of the carrier of R
(y * J) - ((y * J) - (1. R)) is Element of the carrier of R
- ((y * J) - (1. R)) is Element of the carrier of R
(y * J) + (- ((y * J) - (1. R))) is Element of the carrier of R
the addF of R . ((y * J),(- ((y * J) - (1. R)))) is Element of the carrier of R
R is non empty 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 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 left_add-cancelable right_add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
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 V153() V154() V155() V156() doubleLoopStr
the carrier of R is non empty V21() 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 left_add-cancelable right_add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
R is non empty non degenerated V69() 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 V21() set
K32( the carrier of R) is non empty V33() V35() V36() set
{ b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } is set
RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } is Relation-like set
field (RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) is set
dom (RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) is set
rng (RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) is set
(dom (RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } )) \/ (rng (RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } )) is set
x is set
(RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x is Relation-like set
K33(x,x) is set
(RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) /\ K33(x,x) is 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)
{(0. R)} -Ideal is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
I is non empty add-closed left-ideal right-ideal Element of K32( 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
J is set
[J,I] is set
{J,I} is non empty set
{J} is non empty set
{{J,I},{J}} is non empty set
I is set
union x is set
J is set
B is set
A is set
y is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
B is Element of K32( the carrier of R)
y is Element of the carrier of R
A is Element of the carrier of R
y * A 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 . (y,A) is Element of the carrier of R
Aa is set
Ab is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
y is Element of the carrier of R
A is Element of the carrier of R
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( 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 . (A,y) is Element of the carrier of R
Aa is set
Ab is non empty add-closed left-ideal right-ideal Element of K32( 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
A is set
y is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
field ((RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x) is set
dom ((RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x) is set
rng ((RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x) is set
(dom ((RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x)) \/ (rng ((RelIncl { b₁ where b₁ is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R) : b₁ is proper } ) |_2 x)) is set
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
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 . (A,y) is Element of the carrier of R
Aa is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
A + y is Element of the carrier of R
Aa is set
Ab is set
[Aa,Ab] is set
{Aa,Ab} is non empty set
{Aa} is non empty set
{{Aa,Ab},{Aa}} is non empty set
[Ab,Aa] is set
{Ab,Aa} is non empty set
{Ab} is non empty set
{{Ab,Aa},{Ab}} is non empty set
rd is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
sd is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
A is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
y is set
y is set
[y,J] is set
{y,J} is non empty set
{y} is non empty set
{{y,J},{y}} is non empty set
x is set
I is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
J is non empty add-closed left-ideal right-ideal Element of K32( the carrier of R)
[I,J] is Element of K33(K32( the carrier of R),K32( the carrier of R))
K33(K32( the carrier of R),K32( the carrier of R)) is non empty set
{I,J} is non empty set
{I} is non empty set
{{I,J},{I}} is non empty set
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 V153() V154() V155() V156() doubleLoopStr
the carrier of R is non empty V21() set
K32( the carrier of R) is non empty V33() V35() V36() set
the non empty proper add-closed left-ideal right-ideal (R) (R) (R) (R) Element of K32( the carrier of R) is non empty proper add-closed left-ideal right-ideal (R) (R) (R) (R) Element of K32( the carrier of R)
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 V153() V154() V155() V156() doubleLoopStr
the carrier of R is non empty V21() set
K32( the carrier of R) is non empty V33() V35() V36() set
I is non empty add-closed left-ideal right-ideal (R) Element of K32( the carrier of R)
(R,I) is non empty left_add-cancelable right_add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr
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 V153() V154() V155() V156() doubleLoopStr
the carrier of R is non empty V21() set
K32( the carrier of R) is non empty V33() V35() V36() set
I is non empty add-closed left-ideal right-ideal (R) Element of K32( the carrier of R)
(R,I) is non empty left_add-cancelable right_add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V153() V154() V155() V156() doubleLoopStr