:: FVALUAT1 semantic presentation

bool REAL is non empty set
ExtREAL is non empty ext-real-membered set
is non empty set
bool is non empty set
bool ExtREAL is non empty set

bool NAT is non empty set
bool NAT is non empty set
is non empty set
bool is non empty set
bool () is non empty set

bool RAT is non empty set

[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty 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

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

f is ext-real set

R is ext-real set

- R is ext-real set

K + (- v) is complex real ext-real set
f - R is ext-real set
f + (- R) is ext-real set

f is ext-real set

R is ext-real set

R " is 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 * (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 * (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 * (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

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

K is set
K is set
K is ext-real () set
K + 1 is ext-real set
v is ext-real () set

K is ext-real () set

v is non empty ext-real positive non negative () set
f is non empty complex real ext-real positive non negative integer () set

R is non empty ext-real positive non negative () set
S is non empty ext-real positive non negative () 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

bool is non empty set

v is set
rng K is set

K is set
is set
bool is non empty set

f is set
rng v is set

v is set
K . v is set
dom K is set
rng K is set
dom K is set
dom K is set

the carrier of K is non empty 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 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

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

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

b is Element of bool the carrier of K
v *' b is non empty Element of bool the carrier of K
{ K319(K,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 in b ) )
}
is set

y . 1 is set
y /. (len y) is Element of bool the carrier of K
y . (len y) is set

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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 in y ) )
}
is set

R is Element of bool the carrier of K
S is Element of bool the carrier of K

y . (len y) is set
y . 1 is set

b . (len b) is set
b . 1 is set

y . y is set
b . y is set
y . 0 is set
b . 0 is set

y . z is set
b . z is set

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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 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*> . 1 is set

<*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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 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

<*v,(v *' v)*> . 1 is set
<*v,(v *' v)*> . 2 is set

<*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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 in <*v,(v *' v)*> /. R ) )
}
is set

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

(K,v,f) is Element of bool the carrier of K
(K,v,0) is Element of bool 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
[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

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

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 . (len R) is set
R . 1 is set

R . 0 is set

R . S is set

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,b1) where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of K : for b2 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 <= b2 or not b2 <= len b1 or ex b3, b4 being Element of the carrier of K st
( b1 . b2 = b3 * b4 & b3 in v & b4 in R /. S ) )
}
is set

K is non empty doubleLoopStr
the carrier of K is non empty 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

() . (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
() . [v,(abs f)] is set
(() . (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

(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
() . (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
() . [v,f] is set
R is Element of the carrier of K

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,(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
() . [f,(K + 1)] is set

() . (f,K) is set
[f,K] is set
{f,K} is non empty set
{{f,K},{f}} is non empty set
() . [f,K] is set

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

[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
() . [f,R] is set
the multF of v . ((() . (f,R)),f) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of v
[(() . (f,R)),f] is set
{(() . (f,R)),f} is non empty set
{(() . (f,R))} is non empty set
{{(() . (f,R)),f},{(() . (f,R))}} is non empty set
the multF of v . [(() . (f,R)),f] is set

the carrier of f is non empty non trivial set

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
() . (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
() . [R,(K + v)] is set

() . (R,K) is set
[R,K] is set
{R,K} is non empty set
{{R,K},{R}} is non empty set
() . [R,K] is set

() . (R,v) is set
[R,v] is set
{R,v} is non empty set
{{R,v},{R}} is non empty set
() . [R,v] is 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 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

() . (R,0) is set
[R,0] is set
{R,0} is non empty set
{{R,0},{R}} is non empty set
() . [R,0] is set

() . (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
() . [R,(S + 0)] is set

() . (R,S) is set
[R,S] is set
{R,S} is non empty set
{{R,S},{R}} is non empty set
() . [R,S] is set
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

() . (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
() . [R,(S + 0)] is set

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

() . (R,S) is set
[R,S] is set
{R,S} is non empty set
{{R,S},{R}} is non empty set
() . [R,S] is set

() . (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
() . [R,(S + 1)] is set

() . (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
() . [R,(y + (S + 1))] is set

() . (R,y) is set
[R,y] is set
{R,y} is non empty set
{{R,y},{R}} is non empty set
() . [R,y] is set
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

() . (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
() . [R,(y + (S + 1))] is set

() . (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
() . [R,((y + S) + 1)] is set
() . (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
() . [R,(y + S)] is set
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
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
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

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

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,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
() . [f,K] is set

() . (f,0) is set
[f,0] is set
{f,0} is non empty set
{{f,0},{f}} is non empty set
() . [f,0] is set

() . (f,R) is set
[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
() . [f,R] is set

() . (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
() . [f,(R + 1)] is set

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

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,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
() . [f,R] is 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,(abs K)] is set
{f,(abs K)} is non empty set
{f} is non empty set
{{f,(abs K)},{f}} is non empty set
() . [f,(abs K)] is set

() . (f,R) is set
[f,R] is set
{f,R} is non empty set
{{f,R},{f}} is non empty set
() . [f,R] is set

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

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)
v . (1. K) is ext-real () Element of ExtREAL

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

the carrier of K is non empty non trivial set

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

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

the carrier of K is non empty non trivial set

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

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

the carrier of K is non empty non trivial set

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

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

(f . v) + (f . (v ")) is ext-real Element of ExtREAL
f . (1. K) is ext-real () Element of ExtREAL

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

the carrier of K is non empty non trivial 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 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

the carrier of K is non empty non trivial 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 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

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

the carrier of K is non empty non trivial 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 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