:: IDEAL_1 semantic presentation

REAL is V158() V159() V160() V164() V194() V195() V197() set

NAT is non empty non trivial V29() non finite cardinal limit_cardinal V158() V159() V160() V161() V162() V163() V164() V192() V194() Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial V29() non finite cardinal limit_cardinal V158() V159() V160() V161() V162() V163() V164() V192() V194() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

2 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

[:2,2:] is non empty Relation-like RAT -valued INT -valued finite V148() V149() V150() V151() set

RAT is V158() V159() V160() V161() V164() set

INT is V158() V159() V160() V161() V162() V164() set

[:[:2,2:],2:] is non empty Relation-like RAT -valued INT -valued finite V148() V149() V150() V151() set

bool [:[:2,2:],2:] is non empty finite V39() set

COMPLEX is V158() V164() set

INT.Ring is non empty non degenerated non trivial non finite left_add-cancelable right_add-cancelable add-cancelable right_complementable strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like domRing-like gcd-like Euclidian doubleLoopStr

the carrier of INT.Ring is non empty non trivial non finite V158() V159() V160() V161() V162() set

[: the carrier of INT.Ring,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V148() V149() V150() V151() set

bool [: the carrier of INT.Ring,NAT:] is non empty non trivial non finite set

{} is empty trivial Relation-like non-empty empty-yielding RAT -valued functional V29() V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSequence-membered V106() complex ext-real non positive non negative V148() V149() V150() V151() V158() V159() V160() V161() V162() V163() V164() V194() V195() V196() V197() set

the empty trivial Relation-like non-empty empty-yielding RAT -valued functional V29() V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSequence-membered V106() complex ext-real non positive non negative V148() V149() V150() V151() V158() V159() V160() V161() V162() V163() V164() V194() V195() V196() V197() set is empty trivial Relation-like non-empty empty-yielding RAT -valued functional V29() V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSequence-membered V106() complex ext-real non positive non negative V148() V149() V150() V151() V158() V159() V160() V161() V162() V163() V164() V194() V195() V196() V197() set

1 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

3 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

0 is empty trivial Relation-like non-empty empty-yielding RAT -valued functional V29() V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSequence-membered V106() complex ext-real non positive non negative V147() V148() V149() V150() V151() V158() V159() V160() V161() V162() V163() V164() V194() V195() V196() V197() Element of NAT

Seg 1 is non empty trivial finite 1 -element V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of bool NAT

{1} is non empty trivial finite V39() 1 -element V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() set

Seg 2 is non empty finite 2 -element V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of bool NAT

{1,2} is non empty finite V39() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() set

{{}} is non empty trivial finite V39() 1 -element V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() set

the non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

R is non empty add-associative right_zeroed left_zeroed addLoopStr

the carrier of R is non empty set

I is Element of the carrier of R

D is Element of the carrier of R

<*I,D*> is non empty Relation-like NAT -defined the carrier of R -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R

Sum <*I,D*> is Element of the carrier of R

I + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

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

[I,D] is non empty V18() set

{I,D} is non empty finite set

{I} is non empty trivial finite 1 -element set

{{I,D},{I}} is non empty finite V39() set

the addF of R . [I,D] is set

<*I*> is non empty trivial Relation-like NAT -defined the carrier of R -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R

<*D*> is non empty trivial Relation-like NAT -defined the carrier of R -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R

<*I*> ^ <*D*> is non empty Relation-like NAT -defined the carrier of R -valued Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R

1 + 1 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

Sum <*I*> is Element of the carrier of R

Sum <*D*> is Element of the carrier of R

(Sum <*I*>) + (Sum <*D*>) is Element of the carrier of R

the addF of R . ((Sum <*I*>),(Sum <*D*>)) is Element of the carrier of R

[(Sum <*I*>),(Sum <*D*>)] is non empty V18() set

{(Sum <*I*>),(Sum <*D*>)} is non empty finite set

{(Sum <*I*>)} is non empty trivial finite 1 -element set

{{(Sum <*I*>),(Sum <*D*>)},{(Sum <*I*>)}} is non empty finite V39() set

the addF of R . [(Sum <*I*>),(Sum <*D*>)] is set

I + (Sum <*D*>) is Element of the carrier of R

the addF of R . (I,(Sum <*D*>)) is Element of the carrier of R

[I,(Sum <*D*>)] is non empty V18() set

{I,(Sum <*D*>)} is non empty finite set

{{I,(Sum <*D*>)},{I}} is non empty finite V39() set

the addF of R . [I,(Sum <*D*>)] is set

R is non empty addLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

R is non empty multMagma

the carrier of R is non empty set

bool the carrier of R is non empty set

R is non empty addLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

e + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the addF of R . [e,D] is set

R is non empty multMagma

the carrier of R is non empty set

bool the carrier of R is non empty set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

D is Element of the carrier of R

e is Element of the carrier of R

e * D is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the multF of R . [e,D] is set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

D is Element of the carrier of R

e is Element of the carrier of R

D * e is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

R is non empty doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

D is Element of the carrier of R

e is Element of the carrier of R

D * e is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

e is Element of the carrier of R

D is Element of the carrier of R

e + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the addF of R . [e,D] is set

f is Element of the carrier of R

e9 is Element of the carrier of R

e9 * f is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

the multF of R . (e9,f) is Element of the carrier of R

[e9,f] is non empty V18() set

{e9,f} is non empty finite set

{e9} is non empty trivial finite 1 -element set

{{e9,f},{e9}} is non empty finite V39() set

the multF of R . [e9,f] is set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

e + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the addF of R . [e,D] is set

f is Element of the carrier of R

e9 is Element of the carrier of R

f * e9 is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

the multF of R . (f,e9) is Element of the carrier of R

[f,e9] is non empty V18() set

{f,e9} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,e9},{f}} is non empty finite V39() set

the multF of R . [f,e9] is set

D is set

D is Element of bool the carrier of R

e is non empty Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

e + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the addF of R . [e,D] is set

f is Element of the carrier of R

e9 is Element of the carrier of R

e9 * f is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

the multF of R . (e9,f) is Element of the carrier of R

[e9,f] is non empty V18() set

{e9,f} is non empty finite set

{e9} is non empty trivial finite 1 -element set

{{e9,f},{e9}} is non empty finite V39() set

the multF of R . [e9,f] is set

R is non empty commutative multMagma

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

e * D is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the multF of R . [e,D] is set

I is non empty Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

D * e is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

R is non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

0. R is zero left_add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable Element of the carrier of R

I is non empty (R) Element of bool the carrier of R

the Element of I is Element of I

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

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . ((0. R), the Element of I) is left_add-cancelable Element of the carrier of R

[(0. R), the Element of I] is non empty V18() set

{(0. R), the Element of I} is non empty finite set

{(0. R)} is non empty trivial finite 1 -element set

{{(0. R), the Element of I},{(0. R)}} is non empty finite V39() set

the multF of R . [(0. R), the Element of I] is set

R is non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

0. R is zero right_add-cancelable Element of the carrier of R

the ZeroF of R is right_add-cancelable Element of the carrier of R

I is non empty (R) Element of bool the carrier of R

the Element of I is Element of I

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

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . ( the Element of I,(0. R)) is right_add-cancelable Element of the carrier of R

[ the Element of I,(0. R)] is non empty V18() set

{ the Element of I,(0. R)} is non empty finite set

{ the Element of I} is non empty trivial finite 1 -element set

{{ the Element of I,(0. R)},{ the Element of I}} is non empty finite V39() set

the multF of R . [ the Element of I,(0. R)] is set

R is non empty right_zeroed addLoopStr

the carrier of R is non empty set

0. R is zero Element of the carrier of R

the ZeroF of R is Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element Element of bool the carrier of R

bool the carrier of R is non empty set

I is Element of the carrier of R

D is Element of the carrier of R

I + D is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

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

[I,D] is non empty V18() set

{I,D} is non empty finite set

{I} is non empty trivial finite 1 -element set

{{I,D},{I}} is non empty finite V39() set

the addF of R . [I,D] is set

R is non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

0. R is zero right_add-cancelable Element of the carrier of R

the ZeroF of R is right_add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element Element of bool the carrier of R

bool the carrier of R is non empty set

D is right_add-cancelable Element of the carrier of R

I is right_add-cancelable Element of the carrier of R

I * D is right_add-cancelable Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (I,D) is right_add-cancelable Element of the carrier of R

[I,D] is non empty V18() set

{I,D} is non empty finite set

{I} is non empty trivial finite 1 -element set

{{I,D},{I}} is non empty finite V39() set

the multF of R . [I,D] is set

e is right_add-cancelable Element of the carrier of R

e * D is right_add-cancelable Element of the carrier of R

the multF of R . (e,D) is right_add-cancelable Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the multF of R . [e,D] is set

R is non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr

the carrier of R is non empty set

0. R is zero left_add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element Element of bool the carrier of R

bool the carrier of R is non empty set

D is left_add-cancelable Element of the carrier of R

I is left_add-cancelable Element of the carrier of R

D * I is left_add-cancelable Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,I) is left_add-cancelable Element of the carrier of R

[D,I] is non empty V18() set

{D,I} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,I},{D}} is non empty finite V39() set

the multF of R . [D,I] is set

e is left_add-cancelable Element of the carrier of R

D * e is left_add-cancelable Element of the carrier of R

the multF of R . (D,e) is left_add-cancelable Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

R is non empty right_zeroed addLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

0. R is zero Element of the carrier of R

the ZeroF of R is Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element Element of bool the carrier of R

I is Element of bool the carrier of R

R is non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

0. R is zero right_add-cancelable Element of the carrier of R

the ZeroF of R is right_add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element Element of bool the carrier of R

I is Element of bool the carrier of R

R is non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

0. R is zero left_add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) Element of bool the carrier of R

I is Element of bool the carrier of R

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive left-distributive distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) (R) (R) Element of bool the carrier of R

bool the carrier of R is non empty set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) (R) Element of bool the carrier of R

bool the carrier of R is non empty set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) (R) Element of bool the carrier of R

bool the carrier of R is non empty set

R is non empty doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

D * e is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

e is Element of the carrier of R

D is Element of the carrier of R

e * D is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the multF of R . [e,D] is set

D is Element of the carrier of R

e is Element of the carrier of R

D + e is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the addF of R . [D,e] is set

R is non empty doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

D * e is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the multF of R . [D,e] is set

D is Element of the carrier of R

e is Element of the carrier of R

D + e is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the addF of R . [D,e] is set

R is non empty doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is Element of bool the carrier of R

e is Element of the carrier of R

D is Element of the carrier of R

e * D is Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (e,D) is Element of the carrier of R

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

the multF of R . [e,D] is set

D is Element of the carrier of R

e is Element of the carrier of R

D + e is Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (D,e) is Element of the carrier of R

[D,e] is non empty V18() set

{D,e} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,e},{D}} is non empty finite V39() set

the addF of R . [D,e] is set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_zeroed right-distributive left-distributive distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) (R) (R) Element of bool the carrier of R

0. R is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) (R) (R) Element of bool the carrier of R

D is set

{D} is non empty trivial finite 1 -element set

R is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_zeroed right-distributive left-distributive distributive left_zeroed doubleLoopStr

the carrier of R is non empty non trivial set

bool the carrier of R is non empty set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element (R) (R) (R) Element of bool the carrier of R

I is non empty (R) (R) (R) Element of bool the carrier of R

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) Element of bool the carrier of R

D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

1. R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the OneF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- (1. R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

(- (1. R)) * D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . ((- (1. R)),D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(- (1. R)),D] is non empty V18() set

{(- (1. R)),D} is non empty finite set

{(- (1. R))} is non empty trivial finite 1 -element set

{{(- (1. R)),D},{(- (1. R))}} is non empty finite V39() set

the multF of R . [(- (1. R)),D] is set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

(0. R) * D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . ((0. R),D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(0. R),D] is non empty V18() set

{(0. R),D} is non empty finite set

{(0. R)} is non empty trivial finite 1 -element set

{{(0. R),D},{(0. R)}} is non empty finite V39() set

the multF of R . [(0. R),D] is set

(1. R) + (- (1. R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

the addF of R . ((1. R),(- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(1. R),(- (1. R))] is non empty V18() set

{(1. R),(- (1. R))} is non empty finite set

{(1. R)} is non empty trivial finite 1 -element set

{{(1. R),(- (1. R))},{(1. R)}} is non empty finite V39() set

the addF of R . [(1. R),(- (1. R))] is set

((1. R) + (- (1. R))) * D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . (((1. R) + (- (1. R))),D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[((1. R) + (- (1. R))),D] is non empty V18() set

{((1. R) + (- (1. R))),D} is non empty finite set

{((1. R) + (- (1. R)))} is non empty trivial finite 1 -element set

{{((1. R) + (- (1. R))),D},{((1. R) + (- (1. R)))}} is non empty finite V39() set

the multF of R . [((1. R) + (- (1. R))),D] is set

(1. R) * D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . ((1. R),D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(1. R),D] is non empty V18() set

{(1. R),D} is non empty finite set

{{(1. R),D},{(1. R)}} is non empty finite V39() set

the multF of R . [(1. R),D] is set

((1. R) * D) + ((- (1. R)) * D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R . (((1. R) * D),((- (1. R)) * D)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[((1. R) * D),((- (1. R)) * D)] is non empty V18() set

{((1. R) * D),((- (1. R)) * D)} is non empty finite set

{((1. R) * D)} is non empty trivial finite 1 -element set

{{((1. R) * D),((- (1. R)) * D)},{((1. R) * D)}} is non empty finite V39() set

the addF of R . [((1. R) * D),((- (1. R)) * D)] is set

D + ((- (1. R)) * D) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R . (D,((- (1. R)) * D)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,((- (1. R)) * D)] is non empty V18() set

{D,((- (1. R)) * D)} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,((- (1. R)) * D)},{D}} is non empty finite V39() set

the addF of R . [D,((- (1. R)) * D)] is set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive right_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) Element of bool the carrier of R

D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

1. R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the OneF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- (1. R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D * (- (1. R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (D,(- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(- (1. R))] is non empty V18() set

{D,(- (1. R))} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,(- (1. R))},{D}} is non empty finite V39() set

the multF of R . [D,(- (1. R))] is set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D * (0. R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . (D,(0. R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(0. R)] is non empty V18() set

{D,(0. R)} is non empty finite set

{{D,(0. R)},{D}} is non empty finite V39() set

the multF of R . [D,(0. R)] is set

(1. R) + (- (1. R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

the addF of R . ((1. R),(- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(1. R),(- (1. R))] is non empty V18() set

{(1. R),(- (1. R))} is non empty finite set

{(1. R)} is non empty trivial finite 1 -element set

{{(1. R),(- (1. R))},{(1. R)}} is non empty finite V39() set

the addF of R . [(1. R),(- (1. R))] is set

D * ((1. R) + (- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . (D,((1. R) + (- (1. R)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,((1. R) + (- (1. R)))] is non empty V18() set

{D,((1. R) + (- (1. R)))} is non empty finite set

{{D,((1. R) + (- (1. R)))},{D}} is non empty finite V39() set

the multF of R . [D,((1. R) + (- (1. R)))] is set

D * (1. R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the multF of R . (D,(1. R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(1. R)] is non empty V18() set

{D,(1. R)} is non empty finite set

{{D,(1. R)},{D}} is non empty finite V39() set

the multF of R . [D,(1. R)] is set

(D * (1. R)) + (D * (- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R . ((D * (1. R)),(D * (- (1. R)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[(D * (1. R)),(D * (- (1. R)))] is non empty V18() set

{(D * (1. R)),(D * (- (1. R)))} is non empty finite set

{(D * (1. R))} is non empty trivial finite 1 -element set

{{(D * (1. R)),(D * (- (1. R)))},{(D * (1. R))}} is non empty finite V39() set

the addF of R . [(D * (1. R)),(D * (- (1. R)))] is set

D + (D * (- (1. R))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R . (D,(D * (- (1. R)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(D * (- (1. R)))] is non empty V18() set

{D,(D * (- (1. R)))} is non empty finite set

{{D,(D * (- (1. R)))},{D}} is non empty finite V39() set

the addF of R . [D,(D * (- (1. R)))] is set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left-distributive left_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) (R) Element of bool the carrier of R

D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D - e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D + (- e) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (D,(- e)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(- e)] is non empty V18() set

{D,(- e)} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,(- e)},{D}} is non empty finite V39() set

the addF of R . [D,(- e)] is set

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive right_unital left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) (R) Element of bool the carrier of R

D is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D - e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

- e is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

D + (- e) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . (D,(- e)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

[D,(- e)] is non empty V18() set

{D,(- e)} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,(- e)},{D}} is non empty finite V39() set

the addF of R . [D,(- e)] is set

R is non empty left_add-cancelable right_add-cancelable add-cancelable add-associative right_zeroed right-distributive left-distributive distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) (R) Element of bool the carrier of R

D is Element of I

e is V29() V33() V34() finite cardinal V106() complex ext-real non negative V147() V158() V159() V160() V161() V162() V163() V194() V195() V196() Element of NAT

e * D is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

e is V29() V33() V34() finite cardinal V106() complex ext-real non negative V147() V158() V159() V160() V161() V162() V163() V194() V195() V196() Element of NAT

e * D is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

e + 1 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

(e + 1) * D is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

1 * D is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

(1 * D) + (e * D) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R . ((1 * D),(e * D)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

[(1 * D),(e * D)] is non empty V18() set

{(1 * D),(e * D)} is non empty finite set

{(1 * D)} is non empty trivial finite 1 -element set

{{(1 * D),(e * D)},{(1 * D)}} is non empty finite V39() set

the addF of R . [(1 * D),(e * D)] is set

D + (e * D) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the addF of R . (D,(e * D)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

[D,(e * D)] is non empty V18() set

{D,(e * D)} is non empty finite set

{D} is non empty trivial finite 1 -element set

{{D,(e * D)},{D}} is non empty finite V39() set

the addF of R . [D,(e * D)] is set

0 * D is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

0. R is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

R is non empty left_add-cancelable right_add-cancelable add-cancelable right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) Element of bool the carrier of R

D is Element of I

e is V29() V33() V34() finite cardinal V106() complex ext-real non negative V147() V158() V159() V160() V161() V162() V163() V194() V195() V196() Element of NAT

D |^ e is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

e is V29() V33() V34() finite cardinal V106() complex ext-real non negative set

D |^ e is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

e + 1 is non empty V29() V33() V34() finite cardinal V106() complex ext-real positive non negative V147() V158() V159() V160() V161() V162() V163() V192() V193() V194() V195() V196() Element of NAT

D |^ (e + 1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

D |^ 1 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

(D |^ e) * (D |^ 1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . ((D |^ e),(D |^ 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

[(D |^ e),(D |^ 1)] is non empty V18() set

{(D |^ e),(D |^ 1)} is non empty finite set

{(D |^ e)} is non empty trivial finite 1 -element set

{{(D |^ e),(D |^ 1)},{(D |^ e)}} is non empty finite V39() set

the multF of R . [(D |^ e),(D |^ 1)] is set

D |^ 1 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

R is non empty addLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

I is non empty (R) Element of bool the carrier of R

the addF of R || I is Relation-like Function-like set

[:I,I:] is non empty Relation-like set

the addF of R | [:I,I:] is Relation-like [:I,I:] -defined [: the carrier of R, the carrier of R:] -defined the carrier of R -valued set

[:[:I,I:],I:] is non empty Relation-like set

bool [:[:I,I:],I:] is non empty set

[:I,I:] is non empty Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

bool [: the carrier of R, the carrier of R:] is non empty set

[:[:I,I:], the carrier of R:] is non empty Relation-like set

bool [:[:I,I:], the carrier of R:] is non empty set

D is non empty Relation-like [:I,I:] -defined the carrier of R -valued Function-like total V21([:I,I:], the carrier of R) Element of bool [:[:I,I:], the carrier of R:]

dom D is non empty Relation-like I -defined I -valued Element of bool [:I,I:]

bool [:I,I:] is non empty set

e is set

D . e is set

e is set

D is set

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

e9 is Element of the carrier of R

f is Element of the carrier of R

F is Element of the carrier of R

i is Element of the carrier of R

F + i is Element of the carrier of R

the addF of R . (F,i) is Element of the carrier of R

[F,i] is non empty V18() set

{F,i} is non empty finite set

{F} is non empty trivial finite 1 -element set

{{F,i},{F}} is non empty finite V39() set

the addF of R . [F,i] is set

R is non empty multMagma

the carrier of R is non empty set

bool the carrier of R is non empty set

the multF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

I is non empty (R) Element of bool the carrier of R

the multF of R || I is Relation-like Function-like set

[:I,I:] is non empty Relation-like set

the multF of R | [:I,I:] is Relation-like [:I,I:] -defined [: the carrier of R, the carrier of R:] -defined the carrier of R -valued set

[:[:I,I:],I:] is non empty Relation-like set

bool [:[:I,I:],I:] is non empty set

[:I,I:] is non empty Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

bool [: the carrier of R, the carrier of R:] is non empty set

[:[:I,I:], the carrier of R:] is non empty Relation-like set

bool [:[:I,I:], the carrier of R:] is non empty set

D is non empty Relation-like [:I,I:] -defined the carrier of R -valued Function-like total V21([:I,I:], the carrier of R) Element of bool [:[:I,I:], the carrier of R:]

dom D is non empty Relation-like I -defined I -valued Element of bool [:I,I:]

bool [:I,I:] is non empty set

e is set

D . e is set

e is set

D is set

[e,D] is non empty V18() set

{e,D} is non empty finite set

{e} is non empty trivial finite 1 -element set

{{e,D},{e}} is non empty finite V39() set

e9 is Element of I

f is Element of I

[e9,f] is non empty V18() Element of [:I,I:]

{e9,f} is non empty finite set

{e9} is non empty trivial finite 1 -element set

{{e9,f},{e9}} is non empty finite V39() set

the multF of R . [e9,f] is set

e9 * f is Element of the carrier of R

the multF of R . (e9,f) is Element of the carrier of R

[e9,f] is non empty V18() set

the multF of R . [e9,f] is set

R is non empty addLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) Element of bool the carrier of R

(R,I) is non empty Relation-like [:I,I:] -defined I -valued Function-like total V21([:I,I:],I) Element of bool [:[:I,I:],I:]

[:I,I:] is non empty Relation-like set

[:[:I,I:],I:] is non empty Relation-like set

bool [:[:I,I:],I:] is non empty set

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R || I is Relation-like Function-like set

the addF of R | [:I,I:] is Relation-like [:I,I:] -defined [: the carrier of R, the carrier of R:] -defined the carrier of R -valued set

0. R is zero Element of the carrier of R

the ZeroF of R is Element of the carrier of R

In ((0. R),I) is Element of I

addLoopStr(# I,(R,I),(In ((0. R),I)) #) is non empty strict addLoopStr

R is non empty left_add-cancelable right_add-cancelable add-cancelable add-associative right_zeroed right-distributive left-distributive distributive left_zeroed doubleLoopStr

the carrier of R is non empty set

bool the carrier of R is non empty set

I is non empty (R) Element of bool the carrier of R

(R,I) is non empty addLoopStr

(R,I) is non empty Relation-like [:I,I:] -defined I -valued Function-like total V21([:I,I:],I) Element of bool [:[:I,I:],I:]

[:I,I:] is non empty Relation-like set

[:[:I,I:],I:] is non empty Relation-like set

bool [:[:I,I:],I:] is non empty set

the addF of R is non empty Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like total V21([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty Relation-like set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the addF of R || I is Relation-like Function-like set

the addF of R | [:I,I:] is Relation-like [:I,I:] -defined [: the carrier of R, the carrier of R:] -defined the carrier of R -valued set

0. R is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R

In ((0. R),I) is Element of I

addLoopStr(# I,(R,I),(In ((0. R),I)) #) is non empty strict addLoopStr

dom the addF of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

bool [: the carrier of R, the carrier of R:] is non empty set

e is set

[:I,I:] is non empty Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

dom ( the addF of R || I) is set

e is non empty addLoopStr

the carrier of e is non empty set

e is Element of the carrier of e

D is Element of the carrier of e

e + D is Element of the carrier of e

the addF of e is non empty Relation-like [: the carrier of e, the carrier of e:] -defined the carrier of e -valued Function-like total V21([: the carrier of e, the carrier of e:], the carrier of e) Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]

[: the carrier of e, the carrier of e:] is non empty Relation-like set

[:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty Relation-like set

bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set