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

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

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

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 carrier of R is non empty set
I is Element of the carrier of R
D is Element 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

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
() + () is Element of the carrier of R
the addF of R . ((),()) is Element of the carrier of R
[(),()] is non empty V18() set
{(),()} is non empty finite set
{()} is non empty trivial finite 1 -element set
{{(),()},{()}} is non empty finite V39() set
the addF of R . [(),()] is set
I + () is Element of the carrier of R
the addF of R . (I,()) is Element of the carrier of R
[I,()] is non empty V18() set
{I,()} is non empty finite set
{{I,()},{I}} is non empty finite V39() set
the addF of R . [I,()] is set
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
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

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

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

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

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

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

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

the carrier of R is non empty set

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

the carrier of R is non empty set

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

the carrier of R is non empty set

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

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

the carrier of R is non empty non trivial set
bool the carrier of R is non empty set

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

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

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

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

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:]
[(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

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

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

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

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

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:]
[(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

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

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

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

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

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

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

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

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

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

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

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

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

In ((0. R),I) is Element of I
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