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