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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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

( not 1 <= b

( b

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