:: FVALUAT1 semantic presentation

REAL is non empty V26() complex-membered ext-real-membered real-membered add-closed set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty ext-real-membered set
[:NAT,ExtREAL:] is non empty set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
bool NAT is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
RAT is non empty V26() complex-membered ext-real-membered real-membered rational-membered add-closed set
bool RAT is non empty set
COMPLEX is non empty V26() complex-membered add-closed set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT
[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT
{{},1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT
INT is non empty V26() complex-membered ext-real-membered real-membered rational-membered integer-membered add-closed set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer Element of NAT
Seg 1 is non empty V26() V33(1) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
Seg 2 is non empty V26() V33(2) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{1,2} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
len {} is V31() set
K is ext-real set
- K is ext-real set
v is complex real ext-real Element of REAL
- v is complex real ext-real Element of REAL
K is ext-real set
K + K is ext-real set
- K is ext-real set
K is ext-real set
v is ext-real set
f is ext-real set
K * f is ext-real set
R is ext-real set
v * R is ext-real set
v * f is ext-real set
K is complex real ext-real set
f is ext-real set
v is complex real ext-real set
R is ext-real set
- v is complex real ext-real set
- R is ext-real set
K - v is complex real ext-real set
K + (- v) is complex real ext-real set
f - R is ext-real set
f + (- R) is ext-real set
K is complex real ext-real set
f is ext-real set
v is complex real ext-real set
R is ext-real set
v " is complex real ext-real set
R " is ext-real set
K / v is complex real ext-real set
K * (v ") is complex real ext-real set
f / R is ext-real set
f * (R ") is ext-real set
K is ext-real set
v is ext-real set
v / K is ext-real set
K " is ext-real set
v * (K ") is ext-real set
f is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
f / R is complex real ext-real Element of REAL
R " is complex real ext-real set
f * (R ") is complex real ext-real set
K is ext-real set
v is ext-real set
v / K is ext-real set
K " is ext-real set
v * (K ") is ext-real set
R is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
R / f is complex real ext-real Element of REAL
f " is complex real ext-real set
R * (f ") is complex real ext-real set
K is ext-real set
v is ext-real set
v / K is ext-real set
K " is ext-real set
v * (K ") is ext-real set
R is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
R / f is complex real ext-real Element of REAL
f " is complex real ext-real set
R * (f ") is complex real ext-real set
K is ext-real set
v is ext-real set
K + v is ext-real set
f is ext-real set
(K + v) / f is ext-real set
f " is ext-real set
(K + v) * (f ") is ext-real set
K / f is ext-real set
K * (f ") is ext-real set
v / f is ext-real set
v * (f ") is ext-real set
(K / f) + (v / f) is ext-real set
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer Element of REAL
K is ext-real set
v is ext-real set
v / K is ext-real set
K " is ext-real set
v * (K ") is ext-real set
(v / K) * K is ext-real set
1 / K is ext-real set
1 * (K ") is ext-real set
v * (1 / K) is ext-real set
(v * (1 / K)) * K is ext-real set
(1 / K) * K is ext-real set
v * ((1 / K) * K) is ext-real set
v * 1 is ext-real set
K is ext-real set
v is ext-real set
v / K is ext-real set
K " is ext-real set
v * (K ") is ext-real set
K is set
1. is ext-real Element of ExtREAL
K is set
K is set
K is ext-real () set
K + 1 is ext-real set
v is ext-real () set
K + 1. is ext-real set
f is complex real ext-real Element of REAL
f + 1 is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
S is complex real ext-real Element of REAL
y is complex real ext-real Element of REAL
K is ext-real () set
K is ext-real-membered set
v is non empty ext-real positive non negative () set
f is non empty complex real ext-real positive non negative integer () set
f is complex real ext-real integer () set
f is complex real ext-real integer () set
R is non empty ext-real positive non negative () set
S is non empty ext-real positive non negative () set
y is complex real ext-real integer () set
f is non empty ext-real positive non negative () set
f is non empty complex real ext-real positive non negative integer () set
f is non empty ext-real positive non negative () set
R is non empty ext-real positive non negative () set
[:0,ExtREAL:] is set
bool [:0,ExtREAL:] is non empty set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of ExtREAL
0 --> 0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like 0 -defined ExtREAL -valued Function-like functional V26() FinSequence-like FinSubsequence-like FinSequence-membered V38( 0 , ExtREAL ) ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of bool [:0,ExtREAL:]
K is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like 0 -defined ExtREAL -valued Function-like functional V26() FinSequence-like FinSubsequence-like FinSequence-membered V38( 0 , ExtREAL ) ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of bool [:0,ExtREAL:]
v is set
rng K is set
rng K is ext-real-membered Element of bool ExtREAL
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K is set
[:K,ExtREAL:] is set
bool [:K,ExtREAL:] is non empty set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of ExtREAL
K --> 0. is Relation-like K -defined ExtREAL -valued Function-like V38(K, ExtREAL ) Element of bool [:K,ExtREAL:]
v is Relation-like K -defined ExtREAL -valued Function-like V38(K, ExtREAL ) Element of bool [:K,ExtREAL:]
f is set
rng v is set
rng v is ext-real-membered Element of bool ExtREAL
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K is Relation-like Function-like () set
v is set
K . v is set
dom K is set
rng K is set
dom K is set
dom K is set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable right-distributive left-distributive distributive left_unital add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
1. K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the carrier of K is non empty set
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- (1. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(- (1. K)) * (- (1. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((- (1. K)),(- (1. K))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(- (1. K)),(- (1. K))] is set
{(- (1. K)),(- (1. K))} is non empty set
{(- (1. K))} is non empty set
{{(- (1. K)),(- (1. K))},{(- (1. K))}} is non empty set
the multF of K . [(- (1. K)),(- (1. K))] is set
(1. K) * (1. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((1. K),(1. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),(1. K)] is set
{(1. K),(1. K)} is non empty set
{(1. K)} is non empty set
{{(1. K),(1. K)},{(1. K)}} is non empty set
the multF of K . [(1. K),(1. K)] is set
K is non empty doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is Element of bool the carrier of K
[#] K is non empty non proper add-closed left-ideal right-ideal Element of bool the carrier of K
R is non empty non proper add-closed left-ideal right-ideal Element of bool the carrier of K
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
b is Element of bool the carrier of K
v *' b is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in b ) ) } is set
y is Relation-like NAT -defined bool the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
y . 1 is set
y /. (len y) is Element of bool the carrier of K
y . (len y) is set
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
y . (b + 1) is set
y /. b is Element of bool the carrier of K
v *' (y /. b) is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in y /. b ) ) } is set
y . b is set
y is Element of bool the carrier of K
v *' y is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in y ) ) } is set
R is Element of bool the carrier of K
S is Element of bool the carrier of K
y is Relation-like NAT -defined bool the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
y . (len y) is set
y . 1 is set
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
b is Relation-like NAT -defined bool the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
b . (len b) is set
b . 1 is set
dom b is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
y . y is set
b . y is set
y . 0 is set
b . 0 is set
z is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
y . z is set
b . z is set
z + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
y . (z + 1) is set
b . (z + 1) is set
y /. z is Element of bool the carrier of K
b /. z is Element of bool the carrier of K
v *' (y /. z) is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in y /. z ) ) } is set
K is non empty doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
v is Element of bool the carrier of K
(K,v,1) is Element of bool the carrier of K
<*v*> is non empty Relation-like NAT -defined bool the carrier of K -valued Function-like V26() V33(1) FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len <*v*> is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
<*v*> . 1 is set
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
dom <*v*> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
{1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
<*v*> . (R + 1) is set
<*v*> /. R is Element of bool the carrier of K
v *' (<*v*> /. R) is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in <*v*> /. R ) ) } is set
K is non empty doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
v is Element of bool the carrier of K
(K,v,2) is Element of bool the carrier of K
v *' v is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in v ) ) } is set
<*v,(v *' v)*> is non empty Relation-like NAT -defined bool the carrier of K -valued Function-like V26() V33(2) FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len <*v,(v *' v)*> is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
<*v,(v *' v)*> . 1 is set
<*v,(v *' v)*> . 2 is set
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
dom <*v,(v *' v)*> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
{1,2} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
<*v,(v *' v)*> . (R + 1) is set
<*v,(v *' v)*> /. R is Element of bool the carrier of K
v *' (<*v,(v *' v)*> /. R) is non empty Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in <*v,(v *' v)*> /. R ) ) } is set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
v is non empty add-closed left-ideal right-ideal Element of bool the carrier of K
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(K,v,f) is Element of bool the carrier of K
(K,v,0) is Element of bool the carrier of K
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R + S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
the addF of K . [R,S] is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R * S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
the multF of K . [R,S] is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (S,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
the multF of K . [S,R] is set
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
R is Relation-like NAT -defined bool the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of bool the carrier of K
len R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
R . (len R) is set
R . 1 is set
dom R is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
R . 0 is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
R . S is set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
R . (S + 1) is set
R /. S is Element of bool the carrier of K
v *' (R /. S) is non empty add-closed Element of bool the carrier of K
{ K319(K,b₁) where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b₂ being epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or ex b₃, b₄ being Element of the carrier of K st
( b₁ . b₂ = b₃ * b₄ & b₃ in v & b₄ in R /. S ) ) } is set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
K is non empty doubleLoopStr
the carrier of K is non empty set
f is complex real ext-real integer () set
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like V38([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is non empty set
[:[: the carrier of K,NAT:], the carrier of K:] is non empty set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non empty set
v is Element of the carrier of K
abs f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power K) . (v,(abs f)) is Element of the carrier of K
[v,(abs f)] is set
{v,(abs f)} is non empty set
{v} is non empty set
{{v,(abs f)},{v}} is non empty set
(power K) . [v,(abs f)] is set
((power K) . (v,(abs f))) " is Element of the carrier of K
K is non empty doubleLoopStr
the carrier of K is non empty set
v is Element of the carrier of K
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(K,v,f) is Element of the carrier of K
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like V38([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is non empty set
[:[: the carrier of K,NAT:], the carrier of K:] is non empty set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non empty set
(power K) . (v,f) is set
[v,f] is set
{v,f} is non empty set
{v} is non empty set
{{v,f},{v}} is non empty set
(power K) . [v,f] is set
R is Element of the carrier of K
abs f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
K + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(v,f,(K + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
(power v) . (f,(K + 1)) is set
[f,(K + 1)] is set
{f,(K + 1)} is non empty set
{f} is non empty set
{{f,(K + 1)},{f}} is non empty set
(power v) . [f,(K + 1)] is set
(v,f,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,K) is set
[f,K] is set
{f,K} is non empty set
{{f,K},{f}} is non empty set
(power v) . [f,K] is set
(v,f,K) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the multF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is non empty set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
the multF of v . ((v,f,K),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[(v,f,K),f] is set
{(v,f,K),f} is non empty set
{(v,f,K)} is non empty set
{{(v,f,K),f},{(v,f,K)}} is non empty set
the multF of v . [(v,f,K),f] is set
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power v) . (f,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
(power v) . [f,R] is set
((power v) . (f,R)) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the multF of v . (((power v) . (f,R)),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[((power v) . (f,R)),f] is set
{((power v) . (f,R)),f} is non empty set
{((power v) . (f,R))} is non empty set
{{((power v) . (f,R)),f},{((power v) . (f,R))}} is non empty set
the multF of v . [((power v) . (f,R)),f] is set
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
K + v is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
f is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of f is non empty non trivial set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(f,R,(K + v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
power f is Relation-like [: the carrier of f,NAT:] -defined the carrier of f -valued Function-like V38([: the carrier of f,NAT:], the carrier of f) Element of bool [:[: the carrier of f,NAT:], the carrier of f:]
[: the carrier of f,NAT:] is non empty set
[:[: the carrier of f,NAT:], the carrier of f:] is non empty set
bool [:[: the carrier of f,NAT:], the carrier of f:] is non empty set
(power f) . (R,(K + v)) is set
[R,(K + v)] is set
{R,(K + v)} is non empty set
{R} is non empty set
{{R,(K + v)},{R}} is non empty set
(power f) . [R,(K + v)] is set
(f,R,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,K) is set
[R,K] is set
{R,K} is non empty set
{{R,K},{R}} is non empty set
(power f) . [R,K] is set
(f,R,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,v) is set
[R,v] is set
{R,v} is non empty set
{{R,v},{R}} is non empty set
(power f) . [R,v] is set
(f,R,K) * (f,R,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of f . ((f,R,K),(f,R,v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,K),(f,R,v)] is set
{(f,R,K),(f,R,v)} is non empty set
{(f,R,K)} is non empty set
{{(f,R,K),(f,R,v)},{(f,R,K)}} is non empty set
the multF of f . [(f,R,K),(f,R,v)] is set
(f,R,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,0) is set
[R,0] is set
{R,0} is non empty set
{{R,0},{R}} is non empty set
(power f) . [R,0] is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
S + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(f,R,(S + 0)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(S + 0)) is set
[R,(S + 0)] is set
{R,(S + 0)} is non empty set
{{R,(S + 0)},{R}} is non empty set
(power f) . [R,(S + 0)] is set
(f,R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,S) is set
[R,S] is set
{R,S} is non empty set
{{R,S},{R}} is non empty set
(power f) . [R,S] is set
(f,R,S) * (f,R,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,S),(f,R,0)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,S),(f,R,0)] is set
{(f,R,S),(f,R,0)} is non empty set
{(f,R,S)} is non empty set
{{(f,R,S),(f,R,0)},{(f,R,S)}} is non empty set
the multF of f . [(f,R,S),(f,R,0)] is set
S + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () Element of REAL
(f,R,(S + 0)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(S + 0)) is set
[R,(S + 0)] is set
{R,(S + 0)} is non empty set
{{R,(S + 0)},{R}} is non empty set
(power f) . [R,(S + 0)] is set
1_ f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
1. f is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the OneF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(f,R,S) * (1_ f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,S),(1_ f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,S),(1_ f)] is set
{(f,R,S),(1_ f)} is non empty set
{{(f,R,S),(1_ f)},{(f,R,S)}} is non empty set
the multF of f . [(f,R,S),(1_ f)] is set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(f,R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,S) is set
[R,S] is set
{R,S} is non empty set
{{R,S},{R}} is non empty set
(power f) . [R,S] is set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(f,R,(S + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(S + 1)) is set
[R,(S + 1)] is set
{R,(S + 1)} is non empty set
{{R,(S + 1)},{R}} is non empty set
(power f) . [R,(S + 1)] is set
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
y + (S + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () set
(f,R,(y + (S + 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(y + (S + 1))) is set
[R,(y + (S + 1))] is set
{R,(y + (S + 1))} is non empty set
{{R,(y + (S + 1))},{R}} is non empty set
(power f) . [R,(y + (S + 1))] is set
(f,R,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,y) is set
[R,y] is set
{R,y} is non empty set
{{R,y},{R}} is non empty set
(power f) . [R,y] is set
(f,R,y) * (f,R,(S + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,y),(f,R,(S + 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,y),(f,R,(S + 1))] is set
{(f,R,y),(f,R,(S + 1))} is non empty set
{(f,R,y)} is non empty set
{{(f,R,y),(f,R,(S + 1))},{(f,R,y)}} is non empty set
the multF of f . [(f,R,y),(f,R,(S + 1))] is set
y + (S + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(f,R,(y + (S + 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(y + (S + 1))) is set
[R,(y + (S + 1))] is set
{R,(y + (S + 1))} is non empty set
{{R,(y + (S + 1))},{R}} is non empty set
(power f) . [R,(y + (S + 1))] is set
y + S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(y + S) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(f,R,((y + S) + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,((y + S) + 1)) is set
[R,((y + S) + 1)] is set
{R,((y + S) + 1)} is non empty set
{{R,((y + S) + 1)},{R}} is non empty set
(power f) . [R,((y + S) + 1)] is set
(f,R,(y + S)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(power f) . (R,(y + S)) is set
[R,(y + S)] is set
{R,(y + S)} is non empty set
{{R,(y + S)},{R}} is non empty set
(power f) . [R,(y + S)] is set
(f,R,(y + S)) * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,(y + S)),R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,(y + S)),R] is set
{(f,R,(y + S)),R} is non empty set
{(f,R,(y + S))} is non empty set
{{(f,R,(y + S)),R},{(f,R,(y + S))}} is non empty set
the multF of f . [(f,R,(y + S)),R] is set
(f,R,y) * (f,R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,y),(f,R,S)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,y),(f,R,S)] is set
{(f,R,y),(f,R,S)} is non empty set
{{(f,R,y),(f,R,S)},{(f,R,y)}} is non empty set
the multF of f . [(f,R,y),(f,R,S)] is set
((f,R,y) * (f,R,S)) * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . (((f,R,y) * (f,R,S)),R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[((f,R,y) * (f,R,S)),R] is set
{((f,R,y) * (f,R,S)),R} is non empty set
{((f,R,y) * (f,R,S))} is non empty set
{{((f,R,y) * (f,R,S)),R},{((f,R,y) * (f,R,S))}} is non empty set
the multF of f . [((f,R,y) * (f,R,S)),R] is set
(f,R,S) * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,S),R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,S),R] is set
{(f,R,S),R} is non empty set
{(f,R,S)} is non empty set
{{(f,R,S),R},{(f,R,S)}} is non empty set
the multF of f . [(f,R,S),R] is set
(f,R,y) * ((f,R,S) * R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the multF of f . ((f,R,y),((f,R,S) * R)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[(f,R,y),((f,R,S) * R)] is set
{(f,R,y),((f,R,S) * R)} is non empty set
{{(f,R,y),((f,R,S) * R)},{(f,R,y)}} is non empty set
the multF of f . [(f,R,y),((f,R,S) * R)] is set
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
0. v is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the ZeroF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(v,f,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
(power v) . (f,K) is set
[f,K] is set
{f,K} is non empty set
{f} is non empty set
{{f,K},{f}} is non empty set
(power v) . [f,K] is set
(v,f,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,0) is set
[f,0] is set
{f,0} is non empty set
{{f,0},{f}} is non empty set
(power v) . [f,0] is set
1_ v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
1. v is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the OneF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(v,f,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,R) is set
[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
(power v) . [f,R] is set
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(v,f,(R + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,(R + 1)) is set
[f,(R + 1)] is set
{f,(R + 1)} is non empty set
{{f,(R + 1)},{f}} is non empty set
(power v) . [f,(R + 1)] is set
(v,f,R) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the multF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is non empty set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
the multF of v . ((v,f,R),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[(v,f,R),f] is set
{(v,f,R),f} is non empty set
{(v,f,R)} is non empty set
{{(v,f,R),f},{(v,f,R)}} is non empty set
the multF of v . [(v,f,R),f] is set
K is complex real ext-real integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
0. v is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the ZeroF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(v,f,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(v,f,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
(power v) . (f,R) is set
[f,R] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
(power v) . [f,R] is set
- K is complex real ext-real integer () set
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
abs K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power v) . (f,(abs K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[f,(abs K)] is set
{f,(abs K)} is non empty set
{f} is non empty set
{{f,(abs K)},{f}} is non empty set
(power v) . [f,(abs K)] is set
((power v) . (f,(abs K))) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(v,f,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,R) is set
[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
(power v) . [f,R] is set
(v,f,R) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
K is doubleLoopStr
the carrier of K is set
[: the carrier of K,ExtREAL:] is set
bool [: the carrier of K,ExtREAL:] is non empty set
0. K is zero Element of the carrier of K
the ZeroF of K is Element of the carrier of K
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
v . (1. K) is ext-real () Element of ExtREAL
(1. K) * (1. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((1. K),(1. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),(1. K)] is set
{(1. K),(1. K)} is non empty set
{(1. K)} is non empty set
{{(1. K),(1. K)},{(1. K)}} is non empty set
the multF of K . [(1. K),(1. K)] is set
v . ((1. K) * (1. K)) is ext-real () Element of ExtREAL
(v . (1. K)) + (v . (1. K)) is ext-real Element of ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is complex real ext-real Element of REAL
f + 0 is complex real ext-real Element of REAL
f + f is complex real ext-real Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- (1. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
v . (- (1. K)) is ext-real () Element of ExtREAL
(- (1. K)) * (- (1. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((- (1. K)),(- (1. K))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(- (1. K)),(- (1. K))] is set
{(- (1. K)),(- (1. K))} is non empty set
{(- (1. K))} is non empty set
{{(- (1. K)),(- (1. K))},{(- (1. K))}} is non empty set
the multF of K . [(- (1. K)),(- (1. K))] is set
(v . (- (1. K))) + (v . (- (1. K))) is ext-real Element of ExtREAL
v . (1. K) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . (- v) is ext-real () Element of ExtREAL
f . v is ext-real () Element of ExtREAL
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- (1. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(- (1. K)) * v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((- (1. K)),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(- (1. K)),v] is set
{(- (1. K)),v} is non empty set
{(- (1. K))} is non empty set
{{(- (1. K)),v},{(- (1. K))}} is non empty set
the multF of K . [(- (1. K)),v] is set
f . (- (1. K)) is ext-real () Element of ExtREAL
(f . (- (1. K))) + (f . v) is ext-real Element of ExtREAL
0 + (f . v) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . (v ") is ext-real () Element of ExtREAL
f . v is ext-real () Element of ExtREAL
- (f . v) is ext-real Element of ExtREAL
v * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (v,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(v ")] is set
{v,(v ")} is non empty set
{v} is non empty set
{{v,(v ")},{v}} is non empty set
the multF of K . [v,(v ")] is set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(f . v) + (f . (v ")) is ext-real Element of ExtREAL
f . (1. K) is ext-real () Element of ExtREAL
v * (0. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,(0. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(0. K)] is set
{v,(0. K)} is non empty set
{{v,(0. K)},{v}} is non empty set
the multF of K . [v,(0. K)] is set
R is complex real ext-real Element of REAL
S is complex real ext-real Element of REAL
R + S is complex real ext-real Element of REAL
- R is complex real ext-real Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . (f / v) is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
R . v is ext-real () Element of ExtREAL
(R . f) - (R . v) is ext-real Element of ExtREAL
- (R . v) is ext-real set
(R . f) + (- (R . v)) is ext-real set
R . (v ") is ext-real () Element of ExtREAL
(R . f) + (R . (v ")) is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v / f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v * (f ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (v,(f ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(f ")] is set
{v,(f ")} is non empty set
{v} is non empty set
{{v,(f ")},{v}} is non empty set
the multF of K . [v,(f ")] is set
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . (v / f) is ext-real () Element of ExtREAL
R . (f / v) is ext-real () Element of ExtREAL
- (R . (f / v)) is ext-real Element of ExtREAL
R . v is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
(R . v) - (R . f) is ext-real Element of ExtREAL
- (R . f) is ext-real set
(R . v) + (- (R . f)) is ext-real set
(R . f) - (R . v) is ext-real Element of ExtREAL
- (R . v) is ext-real set
(R . f) + (- (R . v)) is ext-real set
- ((R . f) - (R . v)) is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . (f / v) is ext-real () Element of ExtREAL
R . v is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
(R . f) - (R . v) is ext-real Element of ExtREAL
- (R . v) is ext-real set
(R . f) + (- (R . v)) is ext-real set
S is complex real ext-real Element of REAL
y is complex real ext-real Element of REAL
S - y is complex real ext-real Element of REAL
- y is complex real ext-real set
S + (- y) is complex real ext-real set
(S - y) + y is complex real ext-real Element of REAL
(R . (f / v)) + (R . v) is ext-real Element of ExtREAL
0 + (R . v) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v / f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v * (f ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (v,(f ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(f ")] is set
{v,(f ")} is non empty set
{v} is non empty set
{{v,(f ")},{v}} is non empty set
the multF of K . [v,(f ")] is set
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . (v / f) is ext-real () Element of ExtREAL
R . (f / v) is ext-real () Element of ExtREAL
- (R . (f / v)) is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . (f / v) is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
R . v is ext-real () Element of ExtREAL
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v / f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v * (f ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,(f ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(f ")] is set
{v,(f ")} is non empty set
{v} is non empty set
{{v,(f ")},{v}} is non empty set
the multF of K . [v,(f ")] is set
R . (v / f) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v + f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (v,f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,f] is set
{v,f} is non empty set
{v} is non empty set
{{v,f},{v}} is non empty set
the addF of K . [v,f] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . v is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
min ((R . v),(R . f)) is ext-real set
R . (v + f) is ext-real () Element of ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R . (f / v) is ext-real () Element of ExtREAL
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) + (f / v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((1. K),(f / v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),(f / v)] is set
{(1. K),(f / v)} is non empty set
{(1. K)} is non empty set
{{(1. K),(f / v)},{(1. K)}} is non empty set
the addF of K . [(1. K),(f / v)] is set
R . ((1. K) + (f / v)) is ext-real () Element of ExtREAL
0 + (R . v) is ext-real set
(R . ((1. K) + (f / v))) + (R . v) is ext-real Element of ExtREAL
((1. K) + (f / v)) * v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (((1. K) + (f / v)),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[((1. K) + (f / v)),v] is set
{((1. K) + (f / v)),v} is non empty set
{((1. K) + (f / v))} is non empty set
{{((1. K) + (f / v)),v},{((1. K) + (f / v))}} is non empty set
the multF of K . [((1. K) + (f / v)),v] is set
R . (((1. K) + (f / v)) * v) is ext-real () Element of ExtREAL
(1. K) * v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((1. K),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),v] is set
{(1. K),v} is non empty set
{{(1. K),v},{(1. K)}} is non empty set
the multF of K . [(1. K),v] is set
(f / v) * v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((f / v),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(f / v),v] is set
{(f / v),v} is non empty set
{(f / v)} is non empty set
{{(f / v),v},{(f / v)}} is non empty set
the multF of K . [(f / v),v] is set
((1. K) * v) + ((f / v) * v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (((1. K) * v),((f / v) * v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[((1. K) * v),((f / v) * v)] is set
{((1. K) * v),((f / v) * v)} is non empty set
{((1. K) * v)} is non empty set
{{((1. K) * v),((f / v) * v)},{((1. K) * v)}} is non empty set
the addF of K . [((1. K) * v),((f / v) * v)] is set
R . (((1. K) * v) + ((f / v) * v)) is ext-real () Element of ExtREAL
v + ((f / v) * v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (v,((f / v) * v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,((f / v) * v)] is set
{v,((f / v) * v)} is non empty set
{{v,((f / v) * v)},{v}} is non empty set
the addF of K . [v,((f / v) * v)] is set
R . (v + ((f / v) * v)) is ext-real () Element of ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R . (f / v) is ext-real () Element of ExtREAL
v / f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v * (f ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,(f ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(f ")] is set
{v,(f ")} is non empty set
{{v,(f ")},{v}} is non empty set
the multF of K . [v,(f ")] is set
R . (v / f) is ext-real () Element of ExtREAL
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) + (v / f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((1. K),(v / f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),(v / f)] is set
{(1. K),(v / f)} is non empty set
{(1. K)} is non empty set
{{(1. K),(v / f)},{(1. K)}} is non empty set
the addF of K . [(1. K),(v / f)] is set
R . ((1. K) + (v / f)) is ext-real () Element of ExtREAL
0 + (R . f) is ext-real set
(R . ((1. K) + (v / f))) + (R . f) is ext-real Element of ExtREAL
((1. K) + (v / f)) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (((1. K) + (v / f)),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[((1. K) + (v / f)),f] is set
{((1. K) + (v / f)),f} is non empty set
{((1. K) + (v / f))} is non empty set
{{((1. K) + (v / f)),f},{((1. K) + (v / f))}} is non empty set
the multF of K . [((1. K) + (v / f)),f] is set
R . (((1. K) + (v / f)) * f) is ext-real () Element of ExtREAL
(1. K) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((1. K),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),f] is set
{(1. K),f} is non empty set
{{(1. K),f},{(1. K)}} is non empty set
the multF of K . [(1. K),f] is set
(v / f) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((v / f),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v / f),f] is set
{(v / f),f} is non empty set
{(v / f)} is non empty set
{{(v / f),f},{(v / f)}} is non empty set
the multF of K . [(v / f),f] is set
((1. K) * f) + ((v / f) * f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (((1. K) * f),((v / f) * f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[((1. K) * f),((v / f) * f)] is set
{((1. K) * f),((v / f) * f)} is non empty set
{((1. K) * f)} is non empty set
{{((1. K) * f),((v / f) * f)},{((1. K) * f)}} is non empty set
the addF of K . [((1. K) * f),((v / f) * f)] is set
R . (((1. K) * f) + ((v / f) * f)) is ext-real () Element of ExtREAL
f + ((v / f) * f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (f,((v / f) * f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,((v / f) * f)] is set
{f,((v / f) * f)} is non empty set
{{f,((v / f) * f)},{f}} is non empty set
the addF of K . [f,((v / f) * f)] is set
R . (f + ((v / f) * f)) is ext-real () Element of ExtREAL
f + v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (f,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,v] is set
{f,v} is non empty set
{{f,v},{f}} is non empty set
the addF of K . [f,v] is set
R . (f + v) is ext-real () Element of ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R . (f / v) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v + f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (v,f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,f] is set
{v,f} is non empty set
{v} is non empty set
{{v,f},{v}} is non empty set
the addF of K . [v,f] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . f is ext-real () Element of ExtREAL
R . v is ext-real () Element of ExtREAL
R . (v + f) is ext-real () Element of ExtREAL
min ((R . v),(R . f)) is ext-real set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v + (0. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (v,(0. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(0. K)] is set
{v,(0. K)} is non empty set
{{v,(0. K)},{v}} is non empty set
the addF of K . [v,(0. K)] is set
f - f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f + (- f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (f,(- f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(- f)] is set
{f,(- f)} is non empty set
{f} is non empty set
{{f,(- f)},{f}} is non empty set
the addF of K . [f,(- f)] is set
(v + f) - f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(v + f) + (- f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((v + f),(- f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v + f),(- f)] is set
{(v + f),(- f)} is non empty set
{(v + f)} is non empty set
{{(v + f),(- f)},{(v + f)}} is non empty set
the addF of K . [(v + f),(- f)] is set
(v + f) + (- f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R . (- f) is ext-real () Element of ExtREAL
min ((R . (v + f)),(R . f)) is ext-real set
K is complex real ext-real integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
0. v is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the ZeroF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(v,f,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R is Relation-like the carrier of v -defined ExtREAL -valued Function-like V38( the carrier of v, ExtREAL ) () (v)
R . (v,f,K) is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
K * (R . f) is ext-real set
(v,f,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
(power v) . (f,0) is set
[f,0] is set
{f,0} is non empty set
{f} is non empty set
{{f,0},{f}} is non empty set
(power v) . [f,0] is set
1_ v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
1. v is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the OneF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R . (v,f,0) is ext-real () Element of ExtREAL
0 * (R . f) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(v,f,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,S) is set
[f,S] is set
{f,S} is non empty set
{{f,S},{f}} is non empty set
(power v) . [f,S] is set
R . (v,f,S) is ext-real () Element of ExtREAL
S * (R . f) is ext-real set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(v,f,(S + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,(S + 1)) is set
[f,(S + 1)] is set
{f,(S + 1)} is non empty set
{{f,(S + 1)},{f}} is non empty set
(power v) . [f,(S + 1)] is set
R . (v,f,(S + 1)) is ext-real () Element of ExtREAL
(S + 1) * (R . f) is ext-real set
(v,f,S) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the multF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is non empty set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
the multF of v . ((v,f,S),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[(v,f,S),f] is set
{(v,f,S),f} is non empty set
{(v,f,S)} is non empty set
{{(v,f,S),f},{(v,f,S)}} is non empty set
the multF of v . [(v,f,S),f] is set
R . ((v,f,S) * f) is ext-real () Element of ExtREAL
(S * (R . f)) + (R . f) is ext-real set
1. * (R . f) is ext-real Element of ExtREAL
(S * (R . f)) + (1. * (R . f)) is ext-real set
y is ext-real set
y + 1. is ext-real set
(R . f) * (y + 1.) is ext-real set
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(v,f,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,S) is set
[f,S] is set
{f,S} is non empty set
{{f,S},{f}} is non empty set
(power v) . [f,S] is set
R . (v,f,S) is ext-real () Element of ExtREAL
S * (R . f) is ext-real set
- K is complex real ext-real integer () set
abs K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power v) . (f,(abs K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[f,(abs K)] is set
{f,(abs K)} is non empty set
{{f,(abs K)},{f}} is non empty set
(power v) . [f,(abs K)] is set
((power v) . (f,(abs K))) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R . (((power v) . (f,(abs K))) ") is ext-real () Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(v,f,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,S) is set
[f,S] is set
{f,S} is non empty set
{{f,S},{f}} is non empty set
(power v) . [f,S] is set
(v,f,S) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
R . ((v,f,S) ") is ext-real () Element of ExtREAL
R . (v,f,S) is ext-real () Element of ExtREAL
- (R . (v,f,S)) is ext-real Element of ExtREAL
S * (R . f) is ext-real set
- (S * (R . f)) is ext-real set
y is ext-real set
- y is ext-real set
(- y) * (R . f) is ext-real set
- ((- y) * (R . f)) is ext-real set
- (K * (R . f)) is ext-real set
- (- (K * (R . f))) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) + v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((1. K),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),v] is set
{(1. K),v} is non empty set
{(1. K)} is non empty set
{{(1. K),v},{(1. K)}} is non empty set
the addF of K . [(1. K),v] is set
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . ((1. K) + v) is ext-real () Element of ExtREAL
f . v is ext-real () Element of ExtREAL
f . (1. K) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) - v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) + (- v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((1. K),(- v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),(- v)] is set
{(1. K),(- v)} is non empty set
{(1. K)} is non empty set
{{(1. K),(- v)},{(1. K)}} is non empty set
the addF of K . [(1. K),(- v)] is set
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . ((1. K) - v) is ext-real () Element of ExtREAL
f . v is ext-real () Element of ExtREAL
(1. K) + (- v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f . (- v) is ext-real () Element of ExtREAL
K is ext-real () set
v is ext-real () set
v - K is ext-real set
- K is ext-real set
v + (- K) is ext-real set
K + (- K) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f / v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (f,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,(v ")] is set
{f,(v ")} is non empty set
{f} is non empty set
{{f,(v ")},{f}} is non empty set
the multF of K . [f,(v ")] is set
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . v is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
R . (f / v) is ext-real () Element of ExtREAL
(R . f) - (R . v) is ext-real Element of ExtREAL
- (R . v) is ext-real set
(R . f) + (- (R . v)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . (0. K) is ext-real () Element of ExtREAL
dom v is Element of bool the carrier of K
bool the carrier of K is non empty set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
dom f is Element of bool the carrier of K
bool the carrier of K is non empty set
R is non empty ext-real positive non negative () set
S is non empty complex real ext-real positive non negative set
y is complex real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
y is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . R is ext-real () Element of ExtREAL
dom v is Element of bool the carrier of K
bool the carrier of K is non empty set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S is complex real ext-real Element of REAL
S is complex real ext-real Element of REAL
y is complex real ext-real non positive set
R " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . (R ") is ext-real () Element of ExtREAL
- (v . R) is ext-real Element of ExtREAL
b is non empty complex real ext-real non positive negative set
- b is non empty complex real ext-real positive non negative set
S is complex real ext-real Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . f is ext-real () Element of ExtREAL
R is complex real ext-real integer () Element of INT
S is complex real ext-real integer () set
R div S is complex real ext-real integer () set
(R div S) * S is complex real ext-real integer () set
R mod S is complex real ext-real integer () set
((R div S) * S) + (R mod S) is complex real ext-real integer () set
(R div S) * ((rng v)) is ext-real set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
(K,y,(R div S)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,y,(R div S)) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(R div S) * (v . y) is ext-real set
v . (K,y,(R div S)) is ext-real () Element of ExtREAL
- (v . (K,y,(R div S))) is ext-real Element of ExtREAL
v . ((K,y,(R div S)) ") is ext-real () Element of ExtREAL
f * ((K,y,(R div S)) ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (f,((K,y,(R div S)) ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[f,((K,y,(R div S)) ")] is set
{f,((K,y,(R div S)) ")} is non empty set
{f} is non empty set
{{f,((K,y,(R div S)) ")},{f}} is non empty set
the multF of K . [f,((K,y,(R div S)) ")] is set
v . (f * ((K,y,(R div S)) ")) is ext-real () Element of ExtREAL
(v . f) - ((R div S) * S) is ext-real set
- ((R div S) * S) is complex real ext-real set
- ((R div S) * S) is complex real ext-real integer () set
(v . f) + (- ((R div S) * S)) is ext-real set
R - ((R div S) * S) is complex real ext-real integer () set
R + (- ((R div S) * S)) is complex real ext-real integer () set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
{((rng v))} is non empty ext-real-membered set
v " {((rng v))} is Element of bool the carrier of K
bool the carrier of K is non empty set
the Element of v " {((rng v))} is Element of v " {((rng v))}
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
S is complex real ext-real integer () set
R is ext-real Element of ExtREAL
[: the carrier of K,ExtREAL:] is non empty set
bool [: the carrier of K,ExtREAL:] is non empty set
y is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) Element of bool [: the carrier of K,ExtREAL:]
rng y is ext-real-membered Element of bool ExtREAL
b is set
dom y is Element of bool the carrier of K
bool the carrier of K is non empty set
y is set
y . y is set
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y . z is ext-real Element of ExtREAL
v . z is ext-real () Element of ExtREAL
(v . z) / ((rng v)) is ext-real set
((rng v)) " is ext-real non negative set
(v . z) * (((rng v)) ") is ext-real set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
za is complex real ext-real integer () set
za * ((rng v)) is ext-real set
b is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () Element of bool [: the carrier of K,ExtREAL:]
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b . (0. K) is ext-real () set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b . (0. K) is ext-real () Element of ExtREAL
v . (0. K) is ext-real () Element of ExtREAL
(v . (0. K)) / ((rng v)) is ext-real set
((rng v)) " is ext-real non negative set
(v . (0. K)) * (((rng v)) ") is ext-real set
+infty / ((rng v)) is ext-real non negative set
+infty * (((rng v)) ") is ext-real non negative set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b . y is ext-real () Element of ExtREAL
v . y is ext-real () Element of ExtREAL
(v . y) / ((rng v)) is ext-real set
(v . y) * (((rng v)) ") is ext-real set
z is complex real ext-real integer () set
z / S is complex real ext-real set
S " is complex real ext-real set
z * (S ") is complex real ext-real set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b . y is ext-real () Element of ExtREAL
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the multF of K . [y,z] is set
b . (y * z) is ext-real () Element of ExtREAL
b . z is ext-real () Element of ExtREAL
(b . y) + (b . z) is ext-real Element of ExtREAL
v . (y * z) is ext-real () Element of ExtREAL
(v . (y * z)) / ((rng v)) is ext-real set
(v . (y * z)) * (((rng v)) ") is ext-real set
v . y is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
(v . y) + (v . z) is ext-real Element of ExtREAL
((v . y) + (v . z)) / ((rng v)) is ext-real set
((v . y) + (v . z)) * (((rng v)) ") is ext-real set
(v . y) / ((rng v)) is ext-real set
(v . y) * (((rng v)) ") is ext-real set
(v . z) / ((rng v)) is ext-real set
(v . z) * (((rng v)) ") is ext-real set
((v . y) / ((rng v))) + ((v . z) / ((rng v))) is ext-real set
(b . y) + ((v . z) / ((rng v))) is ext-real set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b . y is ext-real () Element of ExtREAL
(1. K) + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . ((1. K),y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),y] is set
{(1. K),y} is non empty set
{(1. K)} is non empty set
{{(1. K),y},{(1. K)}} is non empty set
the addF of K . [(1. K),y] is set
b . ((1. K) + y) is ext-real () Element of ExtREAL
v . ((1. K) + y) is ext-real () Element of ExtREAL
(v . ((1. K) + y)) / ((rng v)) is ext-real set
(v . ((1. K) + y)) * (((rng v)) ") is ext-real set
v . y is ext-real () Element of ExtREAL
(v . y) / ((rng v)) is ext-real set
(v . y) * (((rng v)) ") is ext-real set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
b . y is ext-real () set
b . y is ext-real () Element of ExtREAL
(v . y) / ((rng v)) is ext-real set
(v . y) * (((rng v)) ") is ext-real set
z is complex real ext-real integer () set
y is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . z is ext-real () Element of ExtREAL
y . z is ext-real () Element of ExtREAL
(y . z) * ((rng v)) is ext-real set
(v . z) / ((rng v)) is ext-real set
((rng v)) " is ext-real non negative set
(v . z) * (((rng v)) ") is ext-real set
((v . z) / ((rng v))) * ((rng v)) is ext-real set
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f . S is ext-real () set
R . S is ext-real () set
f . S is ext-real () Element of ExtREAL
(f . S) * ((rng v)) is ext-real set
v . S is ext-real () Element of ExtREAL
R . S is ext-real () Element of ExtREAL
(R . S) * ((rng v)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . v) * ((rng f)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . v) * ((rng f)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
R . v is ext-real () Element of ExtREAL
R . f is ext-real () Element of ExtREAL
(K,R) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,R) . v is ext-real () Element of ExtREAL
(K,R) . f is ext-real () Element of ExtREAL
rng R is ext-real-membered Element of bool ExtREAL
((rng R)) is non empty ext-real positive non negative () set
((K,R) . v) * ((rng R)) is ext-real set
((K,R) . f) * ((rng R)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . v) * ((rng f)) is ext-real set
b is non empty complex real ext-real positive non negative set
y is complex real ext-real Element of REAL
((K,f) . v) * y is ext-real set
y is complex set
z is complex set
y * z is complex set
za is complex real ext-real Element of REAL
za * z is complex set
b is non empty complex real ext-real positive non negative set
y is complex real ext-real Element of REAL
b * y is complex real ext-real Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . v) * ((rng f)) is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,v) . (K,v) is ext-real () Element of ExtREAL
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
v . (K,v) is ext-real () Element of ExtREAL
((K,v) . (K,v)) * ((rng v)) is ext-real set
{((rng v))} is non empty ext-real-membered set
v " {((rng v))} is Element of bool the carrier of K
bool the carrier of K is non empty set
the Element of v " {((rng v))} is Element of v " {((rng v))}
1 * ((rng v)) is non empty ext-real positive non negative set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) . v is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . v) * ((rng f)) is ext-real set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of ExtREAL
0. + 1 is non empty complex real ext-real positive non negative set
0. + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () set
((K,f) . v) * 1 is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,f) . S is ext-real () set
f . S is ext-real () set
f . S is ext-real () Element of ExtREAL
(K,f) . S is ext-real () Element of ExtREAL
rng f is ext-real-membered Element of bool ExtREAL
((rng f)) is non empty ext-real positive non negative () set
((K,f) . S) * ((rng f)) is ext-real set
((K,f) . S) * 1 is ext-real set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,(K,v)) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,(K,v)) . S is ext-real () set
(K,v) . S is ext-real () set
rng (K,v) is ext-real-membered Element of bool ExtREAL
((rng (K,v))) is non empty ext-real positive non negative () set
(K,v) . S is ext-real () Element of ExtREAL
(K,(K,v)) . S is ext-real () Element of ExtREAL
((K,(K,v)) . S) * ((rng (K,v))) is ext-real set
(K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,v) . (K,v) is ext-real () Element of ExtREAL
K is non empty doubleLoopStr
the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
K is non empty doubleLoopStr
the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
f is Element of the carrier of K
v . f is ext-real () Element of ExtREAL
R is Element of the carrier of K
v . R is ext-real () Element of ExtREAL
K is non empty doubleLoopStr
the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
f is set
R is Element of the carrier of K
v . R is ext-real () Element of ExtREAL
K is non empty doubleLoopStr
the carrier of K is non empty set
0. K is zero Element of the carrier of K
the ZeroF of K is Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
v . (0. K) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
v . (1. K) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
[: the carrier of K, the carrier of K:] is non empty set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
[:(K,v),(K,v):] is set
the addF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is set
the addF of K . y is set
za is set
m is set
[za,m] is set
{za,m} is non empty set
{za} is non empty set
{{za,m},{za}} is non empty set
j is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . j is ext-real () Element of ExtREAL
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . z is ext-real () Element of ExtREAL
min ((v . j),(v . z)) is ext-real set
j + z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (j,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[j,z] is set
{j,z} is non empty set
{j} is non empty set
{{j,z},{j}} is non empty set
the addF of K . [j,z] is set
v . (j + z) is ext-real () Element of ExtREAL
y is Preserv of the addF of K
the addF of K || y is Relation-like [:y,y:] -defined y -valued Function-like V38([:y,y:],y) Element of bool [:[:y,y:],y:]
[:y,y:] is set
[:[:y,y:],y:] is set
bool [:[:y,y:],y:] is non empty set
the addF of K | [:y,y:] is Relation-like set
[:[:(K,v),(K,v):],(K,v):] is set
bool [:[:(K,v),(K,v):],(K,v):] is non empty set
za is set
the multF of K . za is set
j is set
z is set
[j,z] is set
{j,z} is non empty set
{j} is non empty set
{{j,z},{j}} is non empty set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . R is ext-real () Element of ExtREAL
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . R is ext-real () Element of ExtREAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of REAL
(v . R) + (v . R) is ext-real Element of ExtREAL
R * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (R,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
the multF of K . [R,R] is set
v . (R * R) is ext-real () Element of ExtREAL
za is Preserv of the multF of K
the multF of K || za is Relation-like [:za,za:] -defined za -valued Function-like V38([:za,za:],za) Element of bool [:[:za,za:],za:]
[:za,za:] is set
[:[:za,za:],za:] is set
bool [:[:za,za:],za:] is non empty set
the multF of K | [:za,za:] is Relation-like set
v . (0. K) is ext-real () Element of ExtREAL
z is Relation-like [:(K,v),(K,v):] -defined (K,v) -valued Function-like V38([:(K,v),(K,v):],(K,v)) Element of bool [:[:(K,v),(K,v):],(K,v):]
m is Relation-like [:(K,v),(K,v):] -defined (K,v) -valued Function-like V38([:(K,v),(K,v):],(K,v)) Element of bool [:[:(K,v),(K,v):],(K,v):]
j is Element of (K,v)
z is Element of (K,v)
doubleLoopStr(# (K,v),z,m,j,z #) is strict doubleLoopStr
R is non empty doubleLoopStr
the carrier of R is non empty set
R is Element of the carrier of R
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x is Element of the carrier of R
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[R,x] is Element of [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
{R,x} is non empty set
{R} is non empty set
{{R,x},{R}} is non empty set
R + x is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (R,x) is Element of the carrier of R
[R,x] is set
the addF of R . [R,x] is set
y + z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of K . [y,z] is set
R is Element of the carrier of R
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x is Element of the carrier of R
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[R,x] is Element of [: the carrier of R, the carrier of R:]
{R,x} is non empty set
{R} is non empty set
{{R,x},{R}} is non empty set
R * x is Element of the carrier of R
the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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 . (R,x) is Element of the carrier of R
[R,x] is set
the multF of R . [R,x] is set
y * z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the multF of K . [y,z] is set
x is Element of the carrier of R
R is Element of the carrier of R
R * x is Element of the carrier of R
the multF of R . (R,x) is Element of the carrier of R
[R,x] is set
{R,x} is non empty set
{R} is non empty set
{{R,x},{R}} is non empty set
the multF of R . [R,x] is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the multF of K . [y,z] is set
x * R is Element of the carrier of R
the multF of R . (x,R) is Element of the carrier of R
[x,R] is set
{x,R} is non empty set
{x} is non empty set
{{x,R},{x}} is non empty set
the multF of R . [x,R] is set
z * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (z,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the multF of K . [z,y] is set
R is Element of the carrier of R
1. R is Element of the carrier of R
the OneF of R is Element of the carrier of R
R * (1. R) is Element of the carrier of R
the multF of R . (R,(1. R)) is Element of the carrier of R
[R,(1. R)] is set
{R,(1. R)} is non empty set
{R} is non empty set
{{R,(1. R)},{R}} is non empty set
the multF of R . [R,(1. R)] is set
(1. R) * R is Element of the carrier of R
the multF of R . ((1. R),R) is Element of the carrier of R
[(1. R),R] is set
{(1. R),R} is non empty set
{(1. R)} is non empty set
{{(1. R),R},{(1. R)}} is non empty set
the multF of R . [(1. R),R] is set
R is non empty unital right_unital well-unital left_unital doubleLoopStr
the carrier of R is non empty set
x is Element of the carrier of R
y is Element of the carrier of R
x + y is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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 set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (x,y) is Element of the carrier of R
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of R . [x,y] is set
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z + x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (z,x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,x1] is set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
the addF of K . [z,x1] is set
y + x is Element of the carrier of R
the addF of R . (y,x) is Element of the carrier of R
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the addF of R . [y,x] is set
x is Element of the carrier of R
y is Element of the carrier of R
z is Element of the carrier of R
y + z is Element of the carrier of R
the addF of R . (y,z) is Element of the carrier of R
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of R . [y,z] is set
y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y1 + z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y1,z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y1,z1] is set
{y1,z1} is non empty set
{y1} is non empty set
{{y1,z1},{y1}} is non empty set
the addF of K . [y1,z1] is set
x + y is Element of the carrier of R
the addF of R . (x,y) is Element of the carrier of R
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of R . [x,y] is set
x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x1 + y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (x1,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the addF of K . [x1,y1] is set
(x + y) + z is Element of the carrier of R
the addF of R . ((x + y),z) is Element of the carrier of R
[(x + y),z] is set
{(x + y),z} is non empty set
{(x + y)} is non empty set
{{(x + y),z},{(x + y)}} is non empty set
the addF of R . [(x + y),z] is set
(x1 + y1) + z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((x1 + y1),z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(x1 + y1),z1] is set
{(x1 + y1),z1} is non empty set
{(x1 + y1)} is non empty set
{{(x1 + y1),z1},{(x1 + y1)}} is non empty set
the addF of K . [(x1 + y1),z1] is set
x1 + (y1 + z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (x1,(y1 + z1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,(y1 + z1)] is set
{x1,(y1 + z1)} is non empty set
{{x1,(y1 + z1)},{x1}} is non empty set
the addF of K . [x1,(y1 + z1)] is set
x + (y + z) is Element of the carrier of R
the addF of R . (x,(y + z)) is Element of the carrier of R
[x,(y + z)] is set
{x,(y + z)} is non empty set
{{x,(y + z)},{x}} is non empty set
the addF of R . [x,(y + z)] is set
x is Element of the carrier of R
0. R is zero Element of the carrier of R
the ZeroF of R is Element of the carrier of R
x + (0. R) is Element of the carrier of R
the addF of R . (x,(0. R)) is Element of the carrier of R
[x,(0. R)] is set
{x,(0. R)} is non empty set
{x} is non empty set
{{x,(0. R)},{x}} is non empty set
the addF of R . [x,(0. R)] is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y + (0. K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y,(0. K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,(0. K)] is set
{y,(0. K)} is non empty set
{y} is non empty set
{{y,(0. K)},{y}} is non empty set
the addF of K . [y,(0. K)] is set
x is Element of the carrier of R
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y + z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of K . [y,z] is set
v . (y + z) is ext-real () Element of ExtREAL
v . y is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
z + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (z,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the addF of K . [z,y] is set
v . (z + y) is ext-real () Element of ExtREAL
x1 is Element of the carrier of R
x + x1 is Element of the carrier of R
the addF of R . (x,x1) is Element of the carrier of R
[x,x1] is set
{x,x1} is non empty set
{x} is non empty set
{{x,x1},{x}} is non empty set
the addF of R . [x,x1] is set
v . y is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
x1 is Element of the carrier of R
x + x1 is Element of the carrier of R
the addF of R . (x,x1) is Element of the carrier of R
[x,x1] is set
{x,x1} is non empty set
{x} is non empty set
{{x,x1},{x}} is non empty set
the addF of R . [x,x1] is set
v . y is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
x is Element of the carrier of R
y is Element of the carrier of R
x * y is Element of the carrier of R
the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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 . (x,y) is Element of the carrier of R
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of R . [x,y] is set
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z * x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (z,x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,x1] is set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
the multF of K . [z,x1] is set
y * x is Element of the carrier of R
the multF of R . (y,x) is Element of the carrier of R
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the multF of R . [y,x] is set
x is Element of the carrier of R
y is Element of the carrier of R
z is Element of the carrier of R
y * z is Element of the carrier of R
the multF of R . (y,z) is Element of the carrier of R
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the multF of R . [y,z] is set
y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y1 * z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y1,z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y1,z1] is set
{y1,z1} is non empty set
{y1} is non empty set
{{y1,z1},{y1}} is non empty set
the multF of K . [y1,z1] is set
x * y is Element of the carrier of R
the multF of R . (x,y) is Element of the carrier of R
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of R . [x,y] is set
x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x1 * y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (x1,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the multF of K . [x1,y1] is set
(x * y) * z is Element of the carrier of R
the multF of R . ((x * y),z) is Element of the carrier of R
[(x * y),z] is set
{(x * y),z} is non empty set
{(x * y)} is non empty set
{{(x * y),z},{(x * y)}} is non empty set
the multF of R . [(x * y),z] is set
(x1 * y1) * z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((x1 * y1),z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(x1 * y1),z1] is set
{(x1 * y1),z1} is non empty set
{(x1 * y1)} is non empty set
{{(x1 * y1),z1},{(x1 * y1)}} is non empty set
the multF of K . [(x1 * y1),z1] is set
x1 * (y1 * z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (x1,(y1 * z1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,(y1 * z1)] is set
{x1,(y1 * z1)} is non empty set
{{x1,(y1 * z1)},{x1}} is non empty set
the multF of K . [x1,(y1 * z1)] is set
x * (y * z) is Element of the carrier of R
the multF of R . (x,(y * z)) is Element of the carrier of R
[x,(y * z)] is set
{x,(y * z)} is non empty set
{{x,(y * z)},{x}} is non empty set
the multF of R . [x,(y * z)] is set
x is Element of the carrier of R
y is Element of the carrier of R
z is Element of the carrier of R
y + z is Element of the carrier of R
the addF of R . (y,z) is Element of the carrier of R
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of R . [y,z] is set
y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y1 + z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y1,z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y1,z1] is set
{y1,z1} is non empty set
{y1} is non empty set
{{y1,z1},{y1}} is non empty set
the addF of K . [y1,z1] is set
x * y is Element of the carrier of R
the multF of R . (x,y) is Element of the carrier of R
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the multF of R . [x,y] is set
x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
x1 * y1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (x1,y1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
the multF of K . [x1,y1] is set
x * z is Element of the carrier of R
the multF of R . (x,z) is Element of the carrier of R
[x,z] is set
{x,z} is non empty set
{{x,z},{x}} is non empty set
the multF of R . [x,z] is set
x1 * z1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (x1,z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,z1] is set
{x1,z1} is non empty set
{{x1,z1},{x1}} is non empty set
the multF of K . [x1,z1] is set
y * x is Element of the carrier of R
the multF of R . (y,x) is Element of the carrier of R
[y,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
the multF of R . [y,x] is set
y1 * x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y1,x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y1,x1] is set
{y1,x1} is non empty set
{{y1,x1},{y1}} is non empty set
the multF of K . [y1,x1] is set
z * x is Element of the carrier of R
the multF of R . (z,x) is Element of the carrier of R
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
the multF of R . [z,x] is set
z1 * x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (z1,x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z1,x1] is set
{z1,x1} is non empty set
{z1} is non empty set
{{z1,x1},{z1}} is non empty set
the multF of K . [z1,x1] is set
x * (y + z) is Element of the carrier of R
the multF of R . (x,(y + z)) is Element of the carrier of R
[x,(y + z)] is set
{x,(y + z)} is non empty set
{{x,(y + z)},{x}} is non empty set
the multF of R . [x,(y + z)] is set
x1 * (y1 + z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (x1,(y1 + z1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[x1,(y1 + z1)] is set
{x1,(y1 + z1)} is non empty set
{{x1,(y1 + z1)},{x1}} is non empty set
the multF of K . [x1,(y1 + z1)] is set
(x1 * y1) + (x1 * z1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((x1 * y1),(x1 * z1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(x1 * y1),(x1 * z1)] is set
{(x1 * y1),(x1 * z1)} is non empty set
{(x1 * y1)} is non empty set
{{(x1 * y1),(x1 * z1)},{(x1 * y1)}} is non empty set
the addF of K . [(x1 * y1),(x1 * z1)] is set
(x * y) + (x * z) is Element of the carrier of R
the addF of R . ((x * y),(x * z)) is Element of the carrier of R
[(x * y),(x * z)] is set
{(x * y),(x * z)} is non empty set
{(x * y)} is non empty set
{{(x * y),(x * z)},{(x * y)}} is non empty set
the addF of R . [(x * y),(x * z)] is set
(y + z) * x is Element of the carrier of R
the multF of R . ((y + z),x) is Element of the carrier of R
[(y + z),x] is set
{(y + z),x} is non empty set
{(y + z)} is non empty set
{{(y + z),x},{(y + z)}} is non empty set
the multF of R . [(y + z),x] is set
(y1 + z1) * x1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((y1 + z1),x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(y1 + z1),x1] is set
{(y1 + z1),x1} is non empty set
{(y1 + z1)} is non empty set
{{(y1 + z1),x1},{(y1 + z1)}} is non empty set
the multF of K . [(y1 + z1),x1] is set
(y1 * x1) + (z1 * x1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . ((y1 * x1),(z1 * x1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(y1 * x1),(z1 * x1)] is set
{(y1 * x1),(z1 * x1)} is non empty set
{(y1 * x1)} is non empty set
{{(y1 * x1),(z1 * x1)},{(y1 * x1)}} is non empty set
the addF of K . [(y1 * x1),(z1 * x1)] is set
(y * x) + (z * x) is Element of the carrier of R
the addF of R . ((y * x),(z * x)) is Element of the carrier of R
[(y * x),(z * x)] is set
{(y * x),(z * x)} is non empty set
{(y * x)} is non empty set
{{(y * x),(z * x)},{(y * x)}} is non empty set
the addF of R . [(y * x),(z * x)] is set
1. R is Element of the carrier of R
the OneF of R is Element of the carrier of R
f is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of f is non empty non trivial set
the addF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
the ZeroF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the OneF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
R is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of R is non empty non trivial set
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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 set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V38([: 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 ZeroF of 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
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,f) is non empty non trivial set
(K,f) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= f . b₁ } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
f is Element of bool the carrier of (K,v)
v .: f is ext-real-membered Element of bool ExtREAL
R is ext-real set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . S is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
the addF of K . [S,y] is set
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
b + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the addF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the addF of (K,v) . (b,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[b,y] is set
{b,y} is non empty set
{b} is non empty set
{{b,y},{b}} is non empty set
the addF of (K,v) . [b,y] is set
[:(K,v),(K,v):] is set
the addF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[b,y] is Element of [: the carrier of (K,v), the carrier of (K,v):]
the addF of (K,v) . [b,y] is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
the multF of K . [S,y] is set
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
b * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the multF of (K,v) . (b,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[b,y] is set
{b,y} is non empty set
{b} is non empty set
{{b,y},{b}} is non empty set
the multF of (K,v) . [b,y] is set
[:(K,v),(K,v):] is set
the multF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[b,y] is Element of [: the carrier of (K,v), the carrier of (K,v):]
the multF of (K,v) . [b,y] is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
0. (K,v) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the carrier of (K,v) is non empty non trivial set
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
1. (K,v) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the carrier of (K,v) is non empty non trivial set
the OneF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
- S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
- y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
v . y is ext-real () set
v . (- S) is ext-real () Element of ExtREAL
v . S is ext-real () Element of ExtREAL
S + (- S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (S,(- S)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[S,(- S)] is set
{S,(- S)} is non empty set
{S} is non empty set
{{S,(- S)},{S}} is non empty set
the addF of K . [S,(- S)] is set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y + b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the addF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the addF of (K,v) . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the addF of (K,v) . [y,b] is set
0. (K,v) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (v,f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,f] is set
{v,f} is non empty set
{v} is non empty set
{{v,f},{v}} is non empty set
the multF of K . [v,f] is set
(v ") * (v * f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((v "),(v * f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v "),(v * f)] is set
{(v "),(v * f)} is non empty set
{(v ")} is non empty set
{{(v "),(v * f)},{(v ")}} is non empty set
the multF of K . [(v "),(v * f)] is set
(v ") * v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((v "),v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v "),v] is set
{(v "),v} is non empty set
{{(v "),v},{(v ")}} is non empty set
the multF of K . [(v "),v] is set
((v ") * v) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (((v ") * v),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[((v ") * v),f] is set
{((v ") * v),f} is non empty set
{((v ") * v)} is non empty set
{{((v ") * v),f},{((v ") * v)}} is non empty set
the multF of K . [((v ") * v),f] is set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((1. K),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),f] is set
{(1. K),f} is non empty set
{(1. K)} is non empty set
{{(1. K),f},{(1. K)}} is non empty set
the multF of K . [(1. K),f] is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(v ") * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((v "),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v "),f] is set
{(v "),f} is non empty set
{(v ")} is non empty set
{{(v "),f},{(v ")}} is non empty set
the multF of K . [(v "),f] is set
v * ((v ") * f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,((v ") * f)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,((v ") * f)] is set
{v,((v ") * f)} is non empty set
{v} is non empty set
{{v,((v ") * f)},{v}} is non empty set
the multF of K . [v,((v ") * f)] is set
v * (v ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,(v ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,(v ")] is set
{v,(v ")} is non empty set
{{v,(v ")},{v}} is non empty set
the multF of K . [v,(v ")] is set
(v * (v ")) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((v * (v ")),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v * (v ")),f] is set
{(v * (v ")),f} is non empty set
{(v * (v "))} is non empty set
{{(v * (v ")),f},{(v * (v "))}} is non empty set
the multF of K . [(v * (v ")),f] is set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(1. K) * f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((1. K),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(1. K),f] is set
{(1. K),f} is non empty set
{(1. K)} is non empty set
{{(1. K),f},{(1. K)}} is non empty set
the multF of K . [(1. K),f] is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
R * S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the multF of (K,v) . (R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
the multF of (K,v) . [R,S] is set
0. (K,v) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
R * S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the multF of K . [y,b] is set
y " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(y ") * (y * b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((y "),(y * b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(y "),(y * b)] is set
{(y "),(y * b)} is non empty set
{(y ")} is non empty set
{{(y "),(y * b)},{(y ")}} is non empty set
the multF of K . [(y "),(y * b)] is set
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
f is Relation-like the carrier of v -defined ExtREAL -valued Function-like V38( the carrier of v, ExtREAL ) () (v)
(v,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (v,f) is non empty non trivial set
power (v,f) is Relation-like [: the carrier of (v,f),NAT:] -defined the carrier of (v,f) -valued Function-like V38([: the carrier of (v,f),NAT:], the carrier of (v,f)) Element of bool [:[: the carrier of (v,f),NAT:], the carrier of (v,f):]
[: the carrier of (v,f),NAT:] is non empty set
[:[: the carrier of (v,f),NAT:], the carrier of (v,f):] is non empty set
bool [:[: the carrier of (v,f),NAT:], the carrier of (v,f):] is non empty set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
(power v) . (S,K) is set
[S,K] is set
{S,K} is non empty set
{S} is non empty set
{{S,K},{S}} is non empty set
(power v) . [S,K] is set
(power (v,f)) . (S,K) is set
(power (v,f)) . [S,K] is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (y,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[y,0] is set
{y,0} is non empty set
{y} is non empty set
{{y,0},{y}} is non empty set
(power v) . [y,0] is set
1_ v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
1. v is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the OneF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power (v,f)) . (S,0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
[S,0] is set
{S,0} is non empty set
{{S,0},{S}} is non empty set
(power (v,f)) . [S,0] is set
1_ (v,f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
1. (v,f) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
the OneF of (v,f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
(power v) . (S,0) is set
(power v) . [S,0] is set
(power (v,f)) . (S,0) is set
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
(power v) . (S,b) is set
[S,b] is set
{S,b} is non empty set
{{S,b},{S}} is non empty set
(power v) . [S,b] is set
(power (v,f)) . (S,b) is set
(power (v,f)) . [S,b] is set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer () Element of REAL
(power v) . (S,(b + 1)) is set
[S,(b + 1)] is set
{S,(b + 1)} is non empty set
{{S,(b + 1)},{S}} is non empty set
(power v) . [S,(b + 1)] is set
(power (v,f)) . (S,(b + 1)) is set
(power (v,f)) . [S,(b + 1)] is set
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power v) . (y,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[y,y] is set
{y,y} is non empty set
{{y,y},{y}} is non empty set
(power v) . [y,y] is set
((power v) . (y,y)) * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the multF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is non empty set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
the multF of v . (((power v) . (y,y)),y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[((power v) . (y,y)),y] is set
{((power v) . (y,y)),y} is non empty set
{((power v) . (y,y))} is non empty set
{{((power v) . (y,y)),y},{((power v) . (y,y))}} is non empty set
the multF of v . [((power v) . (y,y)),y] is set
(power (v,f)) . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
[S,y] is set
{S,y} is non empty set
{{S,y},{S}} is non empty set
(power (v,f)) . [S,y] is set
((power (v,f)) . (S,y)) * S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
the multF of (v,f) is Relation-like [: the carrier of (v,f), the carrier of (v,f):] -defined the carrier of (v,f) -valued Function-like V38([: the carrier of (v,f), the carrier of (v,f):], the carrier of (v,f)) Element of bool [:[: the carrier of (v,f), the carrier of (v,f):], the carrier of (v,f):]
[: the carrier of (v,f), the carrier of (v,f):] is non empty set
[:[: the carrier of (v,f), the carrier of (v,f):], the carrier of (v,f):] is non empty set
bool [:[: the carrier of (v,f), the carrier of (v,f):], the carrier of (v,f):] is non empty set
the multF of (v,f) . (((power (v,f)) . (S,y)),S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
[((power (v,f)) . (S,y)),S] is set
{((power (v,f)) . (S,y)),S} is non empty set
{((power (v,f)) . (S,y))} is non empty set
{{((power (v,f)) . (S,y)),S},{((power (v,f)) . (S,y))}} is non empty set
the multF of (v,f) . [((power (v,f)) . (S,y)),S] is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . (0. K) is ext-real () Element of ExtREAL
{ b₁ where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K : not v . b₁ <= 0 } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
{ b₁ where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K : not v . b₁ <= 0 } is set
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
S is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
S is non empty Element of bool the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . z is ext-real () Element of ExtREAL
y + b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the addF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the addF of (K,v) . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the addF of (K,v) . [y,b] is set
y + z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the addF of K . (y,z) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of K . [y,z] is set
min ((v . y),(v . z)) is ext-real set
v . (y + z) is ext-real () Element of ExtREAL
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
the multF of (K,v) . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the multF of (K,v) . [y,b] is set
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K . (z,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the multF of K . [z,y] is set
v . (z * y) is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
(v . z) + (v . y) is ext-real Element of ExtREAL
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
b * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) . (b,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[b,y] is set
{b,y} is non empty set
{b} is non empty set
{{b,y},{b}} is non empty set
the multF of (K,v) . [b,y] is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
y * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the multF of (K,v) . [y,b] is set
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
z * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (z,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the multF of K . [z,y] is set
v . (z * y) is ext-real () Element of ExtREAL
v . z is ext-real () Element of ExtREAL
(v . z) + (v . y) is ext-real Element of ExtREAL
b * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,f)
(K,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,f) is non empty non trivial set
bool the carrier of (K,f) is non empty set
f . v is ext-real () Element of ExtREAL
{ b₁ where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K : not f . b₁ <= 0 } is set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f . R is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
{ b₁ where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K : not v . b₁ <= 0 } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
{ b₁ where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K : not v . b₁ <= 0 } is set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . f is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
bool the carrier of K is non empty set
f is non empty Element of bool the carrier of K
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
v .: f is non empty ext-real-membered Element of bool ExtREAL
inf (v .: f) is ext-real Element of ExtREAL
{(inf (v .: f))} is non empty ext-real-membered Element of bool ExtREAL
v " {(inf (v .: f))} is Element of bool the carrier of K
(v " {(inf (v .: f))}) /\ f is Element of bool the carrier of K
{ b₁ where b₁ is Element of the carrier of K : ( b₁ in v " {(inf (v .: f))} & b₁ in f ) } is set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
R is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . S is ext-real () Element of ExtREAL
y is non empty ext-real-membered Element of bool ExtREAL
inf y is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
bool the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
f is non empty Element of bool the carrier of K
(K,v,f) is Element of bool the carrier of (K,v)
v .: f is non empty ext-real-membered Element of bool ExtREAL
inf (v .: f) is ext-real Element of ExtREAL
{(inf (v .: f))} is non empty ext-real-membered Element of bool ExtREAL
v " {(inf (v .: f))} is Element of bool the carrier of K
(v " {(inf (v .: f))}) /\ f is Element of bool the carrier of K
{ b₁ where b₁ is Element of the carrier of K : ( b₁ in v " {(inf (v .: f))} & b₁ in f ) } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
bool the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
f is non empty Element of bool the carrier of K
(K,v,f) is Element of bool the carrier of (K,v)
v .: f is non empty ext-real-membered Element of bool ExtREAL
inf (v .: f) is ext-real Element of ExtREAL
{(inf (v .: f))} is non empty ext-real-membered Element of bool ExtREAL
v " {(inf (v .: f))} is Element of bool the carrier of K
(v " {(inf (v .: f))}) /\ f is Element of bool the carrier of K
{ b₁ where b₁ is Element of the carrier of K : ( b₁ in v " {(inf (v .: f))} & b₁ in f ) } is set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . R is ext-real () Element of ExtREAL
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . S is ext-real () Element of ExtREAL
S is ext-real set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
S is ext-real LowerBound of v .: f
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
bool the carrier of K is non empty set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
f is non empty Element of bool the carrier of K
(K,v,f) is Element of bool the carrier of (K,v)
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
{R} is non empty Element of bool the carrier of (K,v)
{R} -Ideal is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
S is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y / b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * (b ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (y,(b ")) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,(b ")] is set
{y,(b ")} is non empty set
{y} is non empty set
{{y,(b ")},{y}} is non empty set
the multF of K . [y,(b ")] is set
v . b is ext-real () Element of ExtREAL
v . y is ext-real () Element of ExtREAL
(v . y) - (v . b) is ext-real Element of ExtREAL
- (v . b) is ext-real set
(v . y) + (- (v . b)) is ext-real set
v . (y / b) is ext-real () Element of ExtREAL
b * (y / b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (b,(y / b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[b,(y / b)] is set
{b,(y / b)} is non empty set
{b} is non empty set
{{b,(y / b)},{b}} is non empty set
the multF of K . [b,(y / b)] is set
(b ") * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . ((b "),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(b "),b] is set
{(b "),b} is non empty set
{(b ")} is non empty set
{{(b "),b},{(b ")}} is non empty set
the multF of K . [(b "),b] is set
y * ((b ") * b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y,((b ") * b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,((b ") * b)] is set
{y,((b ") * b)} is non empty set
{{y,((b ") * b)},{y}} is non empty set
the multF of K . [y,((b ") * b)] is set
1_ K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * (1_ K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y,(1_ K)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,(1_ K)] is set
{y,(1_ K)} is non empty set
{{y,(1_ K)},{y}} is non empty set
the multF of K . [y,(1_ K)] is set
za is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
R * za is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the multF of (K,v) . (R,za) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[R,za] is set
{R,za} is non empty set
{R} is non empty set
{{R,za},{R}} is non empty set
the multF of (K,v) . [R,za] is set
{ (R * b₁) where b₁ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v) : verum } is set
0. (K,v) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
{(0. (K,v))} is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . b is ext-real () Element of ExtREAL
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . y is ext-real () Element of ExtREAL
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
0. (K,v) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
K is non empty doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
v is non empty add-closed Element of bool the carrier of K
f is set
[:v,v:] is non empty set
the addF of K . f is set
R is set
S is set
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
y is Element of v
b is Element of v
y + b is Element of the carrier of K
the addF of K . (y,b) is Element of the carrier of K
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the addF of K . [y,b] is set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
RightModule K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() RightModStr over K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
RightModStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict RightModStr over K
v is non empty add-closed right-ideal Element of bool the carrier of K
the carrier of (RightModule K) is non empty set
bool the carrier of (RightModule K) is non empty set
f is Element of bool the carrier of (RightModule K)
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y + b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the addF of K . (y,b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,b] is set
{y,b} is non empty set
{y} is non empty set
{{y,b},{y}} is non empty set
the addF of K . [y,b] is set
R + S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
the addF of (RightModule K) is Relation-like [: the carrier of (RightModule K), the carrier of (RightModule K):] -defined the carrier of (RightModule K) -valued Function-like V38([: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K)) Element of bool [:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):]
[: the carrier of (RightModule K), the carrier of (RightModule K):] is non empty set
[:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):] is non empty set
bool [:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):] is non empty set
the addF of (RightModule K) . (R,S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
[R,S] is set
{R,S} is non empty set
{R} is non empty set
{{R,S},{R}} is non empty set
the addF of (RightModule K) . [R,S] is set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
S * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
the rmult of (RightModule K) is Relation-like [: the carrier of (RightModule K), the carrier of K:] -defined the carrier of (RightModule K) -valued Function-like V38([: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K)) Element of bool [:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):]
[: the carrier of (RightModule K), the carrier of K:] is non empty set
[:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):] is non empty set
bool [:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):] is non empty set
the rmult of (RightModule K) . (S,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
[S,R] is set
{S,R} is non empty set
{S} is non empty set
{{S,R},{S}} is non empty set
the rmult of (RightModule K) . [S,R] is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (y,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[y,R] is set
{y,R} is non empty set
{y} is non empty set
{{y,R},{y}} is non empty set
the multF of K . [y,R] is set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
RightModule K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() RightModStr over K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
RightModStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict RightModStr over K
v is non empty add-closed right-ideal Element of bool the carrier of K
f is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() Submodule of RightModule K
the carrier of f is non empty set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
v is non empty add-closed right-ideal Element of bool the carrier of K
RightModule K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() RightModStr over K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
RightModStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict RightModStr over K
f is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() Submodule of RightModule K
the carrier of f is non empty set
the addF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the ZeroF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the rmult of f is Relation-like [: the carrier of f, the carrier of K:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of K:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of K:], the carrier of f:]
[: the carrier of f, the carrier of K:] is non empty set
[:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
RightModStr(# the carrier of f, the addF of f, the ZeroF of f, the rmult of f #) is non empty strict RightModStr over K
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() (K,v)
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of K is non empty set
bool the carrier of K is non empty set
[: the carrier of K, the carrier of K:] is non empty set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is non empty add-closed left-ideal right-ideal Element of bool the carrier of K
[:v,v:] is non empty set
[:[:v,v:],v:] is non empty set
bool [:[:v,v:],v:] is non empty set
[:v, the carrier of K:] is non empty set
[:[:v, the carrier of K:],v:] is non empty set
bool [:[:v, the carrier of K:],v:] is non empty set
the addF of K | [:v,v:] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K | [:v, the carrier of K:] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
f is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() (K,v)
the carrier of f is non empty set
the addF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the ZeroF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the rmult of f is Relation-like [: the carrier of f, the carrier of K:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of K:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of K:], the carrier of f:]
[: the carrier of f, the carrier of K:] is non empty set
[:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
RightModStr(# the carrier of f, the addF of f, the ZeroF of f, the rmult of f #) is non empty strict RightModStr over K
RightModule K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() RightModStr over K
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
RightModStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is non empty strict RightModStr over K
0. f is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
0. (RightModule K) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
the carrier of (RightModule K) is non empty set
the ZeroF of (RightModule K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (RightModule K)
[: the carrier of (RightModule K), the carrier of (RightModule K):] is non empty set
the addF of (RightModule K) is Relation-like [: the carrier of (RightModule K), the carrier of (RightModule K):] -defined the carrier of (RightModule K) -valued Function-like V38([: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K)) Element of bool [:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):]
[:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):] is non empty set
bool [:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):] is non empty set
the addF of (RightModule K) | [:v,v:] is Relation-like [: the carrier of (RightModule K), the carrier of (RightModule K):] -defined the carrier of (RightModule K) -valued Function-like Element of bool [:[: the carrier of (RightModule K), the carrier of (RightModule K):], the carrier of (RightModule K):]
[: the carrier of (RightModule K), the carrier of K:] is non empty set
the rmult of (RightModule K) is Relation-like [: the carrier of (RightModule K), the carrier of K:] -defined the carrier of (RightModule K) -valued Function-like V38([: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K)) Element of bool [:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):]
[:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):] is non empty set
bool [:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):] is non empty set
the rmult of (RightModule K) | [:v, the carrier of K:] is Relation-like [: the carrier of (RightModule K), the carrier of K:] -defined the carrier of (RightModule K) -valued Function-like Element of bool [:[: the carrier of (RightModule K), the carrier of K:], the carrier of (RightModule K):]
S is Relation-like [:v,v:] -defined v -valued Function-like V38([:v,v:],v) Element of bool [:[:v,v:],v:]
b is Relation-like [:v, the carrier of K:] -defined v -valued Function-like V38([:v, the carrier of K:],v) Element of bool [:[:v, the carrier of K:],v:]
y is Element of v
RightModStr(# v,S,y,b #) is non empty strict RightModStr over K
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
v is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() RightModStr over K
the carrier of v is non empty set
f is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() RightModStr over K
the carrier of f is non empty set
[: the carrier of v, the carrier of f:] is non empty set
bool [: the carrier of v, the carrier of f:] is non empty set
K is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
v is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() RightModStr over K
f is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed RightMod-like V235() V236() V237() V238() Submodule of v
incl (f,v) is Relation-like the carrier of f -defined the carrier of v -valued Function-like V38( the carrier of f, the carrier of v) Element of bool [: the carrier of f, the carrier of v:]
the carrier of f is non empty set
the carrier of v is non empty set
[: the carrier of f, the carrier of v:] is non empty set
bool [: the carrier of f, the carrier of v:] is non empty set
id the carrier of f is non empty Relation-like the carrier of f -defined the carrier of f -valued total Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
S + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the addF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
the addF of f . [S,y] is set
(incl (f,v)) . (S + y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(incl (f,v)) . S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(incl (f,v)) . y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
((incl (f,v)) . S) + ((incl (f,v)) . y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the addF of v is Relation-like [: the carrier of v, the carrier of v:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of v:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of v:], the carrier of v:]
[: the carrier of v, the carrier of v:] is non empty set
[:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of v:], the carrier of v:] is non empty set
the addF of v . (((incl (f,v)) . S),((incl (f,v)) . y)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[((incl (f,v)) . S),((incl (f,v)) . y)] is set
{((incl (f,v)) . S),((incl (f,v)) . y)} is non empty set
{((incl (f,v)) . S)} is non empty set
{{((incl (f,v)) . S),((incl (f,v)) . y)},{((incl (f,v)) . S)}} is non empty set
the addF of v . [((incl (f,v)) . S),((incl (f,v)) . y)] is set
S + y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(incl (f,v)) . (S + y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the carrier of K is non empty set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
(incl (f,v)) . S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the rmult of f is Relation-like [: the carrier of f, the carrier of K:] -defined the carrier of f -valued Function-like V38([: the carrier of f, the carrier of K:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of K:], the carrier of f:]
[: the carrier of f, the carrier of K:] is non empty set
[:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of K:], the carrier of f:] is non empty set
the rmult of f . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
the rmult of f . [S,y] is set
(incl (f,v)) . (S * y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
((incl (f,v)) . S) * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the rmult of v is Relation-like [: the carrier of v, the carrier of K:] -defined the carrier of v -valued Function-like V38([: the carrier of v, the carrier of K:], the carrier of v) Element of bool [:[: the carrier of v, the carrier of K:], the carrier of v:]
[: the carrier of v, the carrier of K:] is non empty set
[:[: the carrier of v, the carrier of K:], the carrier of v:] is non empty set
bool [:[: the carrier of v, the carrier of K:], the carrier of v:] is non empty set
the rmult of v . (((incl (f,v)) . S),y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[((incl (f,v)) . S),y] is set
{((incl (f,v)) . S),y} is non empty set
{((incl (f,v)) . S)} is non empty set
{{((incl (f,v)) . S),y},{((incl (f,v)) . S)}} is non empty set
the rmult of v . [((incl (f,v)) . S),y] is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
R is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,R) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,R) is non empty non trivial set
R . f is ext-real () Element of ExtREAL
R . v is ext-real () Element of ExtREAL
(R . f) + (R . v) is ext-real Element of ExtREAL
(R . f) + 0 is ext-real set
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (f,K) is set
[f,K] is set
{f,K} is non empty set
{f} is non empty set
{{f,K},{f}} is non empty set
(power v) . [f,K] is set
R is Relation-like the carrier of v -defined ExtREAL -valued Function-like V38( the carrier of v, ExtREAL ) () (v)
(v,R) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (v,R) is non empty non trivial set
power (v,R) is Relation-like [: the carrier of (v,R),NAT:] -defined the carrier of (v,R) -valued Function-like V38([: the carrier of (v,R),NAT:], the carrier of (v,R)) Element of bool [:[: the carrier of (v,R),NAT:], the carrier of (v,R):]
[: the carrier of (v,R),NAT:] is non empty set
[:[: the carrier of (v,R),NAT:], the carrier of (v,R):] is non empty set
bool [:[: the carrier of (v,R),NAT:], the carrier of (v,R):] is non empty set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,R)
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered integer () Element of NAT
(power (v,R)) . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,R)
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
(power (v,R)) . [S,y] is set
K is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer () set
v is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of v is non empty non trivial set
0. v is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
the ZeroF of v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
power v is Relation-like [: the carrier of v,NAT:] -defined the carrier of v -valued Function-like V38([: the carrier of v,NAT:], the carrier of v) Element of bool [:[: the carrier of v,NAT:], the carrier of v:]
[: the carrier of v,NAT:] is non empty set
[:[: the carrier of v,NAT:], the carrier of v:] is non empty set
bool [:[: the carrier of v,NAT:], the carrier of v:] is non empty set
f is Relation-like the carrier of v -defined ExtREAL -valued Function-like V38( the carrier of v, ExtREAL ) () (v)
(v,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (v,f) is non empty non trivial set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (v,f)
(power v) . (R,K) is set
[R,K] is set
{R,K} is non empty set
{R} is non empty set
{{R,K},{R}} is non empty set
(power v) . [R,K] is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
(power v) . (S,K) is set
[S,K] is set
{S,K} is non empty set
{S} is non empty set
{{S,K},{S}} is non empty set
(power v) . [S,K] is set
(v,S,K) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,f) is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f . (v ") is ext-real () Element of ExtREAL
- (f . v) is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,f) is non empty non trivial set
f . v is ext-real () Element of ExtREAL
f . (v ") is ext-real () Element of ExtREAL
- (f . v) is ext-real Element of ExtREAL
- (- (f . v)) is ext-real Element of ExtREAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real functional FinSequence-membered ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed integer () Element of REAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
f . v is ext-real () Element of ExtREAL
(K,f) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,f) is non empty non trivial set
bool the carrier of (K,f) is non empty set
R is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,f)
S is set
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
z is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
z * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
the multF of (K,f) is Relation-like [: the carrier of (K,f), the carrier of (K,f):] -defined the carrier of (K,f) -valued Function-like V38([: the carrier of (K,f), the carrier of (K,f):], the carrier of (K,f)) Element of bool [:[: the carrier of (K,f), the carrier of (K,f):], the carrier of (K,f):]
[: the carrier of (K,f), the carrier of (K,f):] is non empty set
[:[: the carrier of (K,f), the carrier of (K,f):], the carrier of (K,f):] is non empty set
bool [:[: the carrier of (K,f), the carrier of (K,f):], the carrier of (K,f):] is non empty set
the multF of (K,f) . (z,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
the multF of (K,f) . [z,y] is set
y * (z * y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
the multF of (K,f) . (y,(z * y)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,f)
[y,(z * y)] is set
{y,(z * y)} is non empty set
{y} is non empty set
{{y,(z * y)},{y}} is non empty set
the multF of (K,f) . [y,(z * y)] is set
b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(v ") * b is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . ((v "),b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[(v "),b] is set
{(v "),b} is non empty set
{(v ")} is non empty set
{{(v "),b},{(v ")}} is non empty set
the multF of K . [(v "),b] is set
v * ((v ") * b) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K . (v,((v ") * b)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[v,((v ") * b)] is set
{v,((v ") * b)} is non empty set
{v} is non empty set
{{v,((v ") * b)},{v}} is non empty set
the multF of K . [v,((v ") * b)] is set
(K,f) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= f . b₁ } is set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
rng v is ext-real-membered Element of bool ExtREAL
((rng v)) is non empty ext-real positive non negative () set
{((rng v))} is non empty ext-real-membered set
v " {((rng v))} is Element of bool the carrier of K
bool the carrier of K is non empty set
the Element of v " {((rng v))} is Element of v " {((rng v))}
v . (K,v) is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
bool the carrier of (K,v) is non empty set
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
bool the carrier of (K,v) is non empty set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
v . f is ext-real () set
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . R is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
f * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
the multF of (K,v) . (f,R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
[f,R] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
the multF of (K,v) . [f,R] is set
f * R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
v . f is ext-real () set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
S * y is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the multF of K . (S,y) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
[S,y] is set
{S,y} is non empty set
{S} is non empty set
{{S,y},{S}} is non empty set
the multF of K . [S,y] is set
v . y is ext-real () Element of ExtREAL
v . (S * y) is ext-real () Element of ExtREAL
v . S is ext-real () Element of ExtREAL
(v . S) + (v . y) is ext-real Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
f is non empty proper add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
R is set
v . R is ext-real () set
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
1. (K,v) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the OneF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
f is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,v) is non empty non trivial set
bool the carrier of (K,v) is non empty set
(K,v) is non empty add-closed left-ideal right-ideal Element of bool the carrier of (K,v)
f is non empty proper add-closed left-ideal right-ideal V250((K,v)) prime V252((K,v)) maximal Element of bool the carrier of (K,v)
1. (K,v) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
the OneF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,(K,v)) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= (K,v) . b₁ } is set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
R is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
(K,v) . S is ext-real () Element of ExtREAL
v . S is ext-real () Element of ExtREAL
R is set
S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
v . S is ext-real () Element of ExtREAL
(K,v) . S is ext-real () Element of ExtREAL
K is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() Field-like doubleLoopStr
the carrier of K is non empty non trivial set
v is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,v) is Relation-like the carrier of K -defined ExtREAL -valued Function-like V38( the carrier of K, ExtREAL ) () (K)
(K,(K,v)) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
(K,v) is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V235() V236() V237() V238() doubleLoopStr
the carrier of (K,(K,v)) is non empty non trivial set
(K,(K,v)) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= (K,v) . b₁ } is set
(K,v) is set
{ b₁ where b₁ is Element of the carrier of K : 0 <= v . b₁ } is set
the addF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
the carrier of (K,v) is non empty non trivial set
[: the carrier of (K,v), the carrier of (K,v):] is non empty set
[:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):] is non empty set
[: the carrier of K, the carrier of K:] is non empty set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
[:(K,v),(K,v):] is set
the addF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the addF of (K,(K,v)) is Relation-like [: the carrier of (K,(K,v)), the carrier of (K,(K,v)):] -defined the carrier of (K,(K,v)) -valued Function-like V38([: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v))) Element of bool [:[: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v)):]
[: the carrier of (K,(K,v)), the carrier of (K,(K,v)):] is non empty set
[:[: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v)):] is non empty set
bool [:[: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v)):] is non empty set
the multF of (K,v) is Relation-like [: the carrier of (K,v), the carrier of (K,v):] -defined the carrier of (K,v) -valued Function-like V38([: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v)) Element of bool [:[: the carrier of (K,v), the carrier of (K,v):], the carrier of (K,v):]
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V38([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of K | [:(K,v),(K,v):] is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the multF of (K,(K,v)) is Relation-like [: the carrier of (K,(K,v)), the carrier of (K,(K,v)):] -defined the carrier of (K,(K,v)) -valued Function-like V38([: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v))) Element of bool [:[: the carrier of (K,(K,v)), the carrier of (K,(K,v)):], the carrier of (K,(K,v)):]
the ZeroF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
0. K is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the ZeroF of (K,(K,v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,(K,v))
the OneF of (K,v) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,v)
1. K is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of K is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of K
the OneF of (K,(K,v)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (K,(K,v))