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