:: SEQ_4 semantic presentation

REAL is non empty non trivial complex-membered ext-real-membered real-membered V56() non finite non bounded_below non bounded_above V71() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() non finite left_end bounded_below cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite set

COMPLEX is non empty non trivial complex-membered V56() non finite set

RAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered V56() non finite set

INT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered V56() non finite set

[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial complex-valued non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial complex-valued non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:REAL,REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued natural-valued non finite set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial complex-valued ext-real-valued real-valued natural-valued non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() non finite left_end bounded_below cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

ExtREAL is non empty ext-real-membered V71() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite left_end right_end bounded_below bounded_above real-bounded cardinal Element of NAT

[:NAT,REAL:] is Relation-like non empty non trivial complex-valued ext-real-valued real-valued non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

bool [:NAT,NAT:] is non empty non trivial non finite set

dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty trivial Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

|.0.| is complex real ext-real V49() Element of REAL

Re 0 is complex real ext-real Element of REAL

(Re 0) ^2 is complex real ext-real Element of REAL

(Re 0) * (Re 0) is complex real ext-real set

Im 0 is complex real ext-real Element of REAL

(Im 0) ^2 is complex real ext-real Element of REAL

(Im 0) * (Im 0) is complex real ext-real set

((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL

sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL

sqrt 0 is complex real ext-real Element of REAL

compcomplex is Relation-like COMPLEX -defined COMPLEX -valued Function-like non empty total V18( COMPLEX , COMPLEX ) complex-valued Element of bool [:COMPLEX,COMPLEX:]

addcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued commutative associative V79( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

diffcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

multcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like non empty total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued commutative associative V79( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

the_unity_wrt addcomplex is complex Element of COMPLEX

the_unity_wrt multcomplex is complex Element of COMPLEX

card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

R is complex-membered ext-real-membered real-membered Element of bool REAL

r0 is complex-membered ext-real-membered real-membered Element of bool REAL

r1 is complex real ext-real set

t is complex real ext-real set

r1 is complex real ext-real set

t is complex real ext-real Element of REAL

t is complex real ext-real set

m is complex real ext-real set

R is complex real ext-real set

r0 is complex-membered ext-real-membered real-membered Element of bool REAL

r1 is complex-membered ext-real-membered real-membered Element of bool REAL

t is complex real ext-real set

t is complex real ext-real set

t + R is complex real ext-real Element of REAL

t + 0 is complex real ext-real Element of REAL

t is complex real ext-real set

t is complex real ext-real set

t is complex real ext-real set

t - R is complex real ext-real Element of REAL

m is complex real ext-real set

m + R is complex real ext-real Element of REAL

(t - R) + R is complex real ext-real Element of REAL

- 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() finite finite-yielding V61() bounded_below bounded_above real-bounded V71() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of REAL

- R is complex real ext-real Element of REAL

t + 0 is complex real ext-real Element of REAL

t + (- R) is complex real ext-real Element of REAL

m is complex real ext-real set

R is complex real ext-real set

r0 is complex real ext-real set

r0 + 1 is complex real ext-real Element of REAL

r0 is complex real ext-real set

r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R is complex-membered ext-real-membered real-membered Element of bool REAL

r0 is complex real ext-real set

r1 is complex real ext-real set

r1 is complex real ext-real set

t is complex real ext-real set

abs r0 is complex real ext-real Element of REAL

Re r0 is complex real ext-real Element of REAL

(Re r0) ^2 is complex real ext-real Element of REAL

(Re r0) * (Re r0) is complex real ext-real set

Im r0 is complex real ext-real Element of REAL

(Im r0) ^2 is complex real ext-real Element of REAL

(Im r0) * (Im r0) is complex real ext-real set

((Re r0) ^2) + ((Im r0) ^2) is complex real ext-real Element of REAL

sqrt (((Re r0) ^2) + ((Im r0) ^2)) is complex real ext-real Element of REAL

abs r1 is complex real ext-real Element of REAL

Re r1 is complex real ext-real Element of REAL

(Re r1) ^2 is complex real ext-real Element of REAL

(Re r1) * (Re r1) is complex real ext-real set

Im r1 is complex real ext-real Element of REAL

(Im r1) ^2 is complex real ext-real Element of REAL

(Im r1) * (Im r1) is complex real ext-real set

((Re r1) ^2) + ((Im r1) ^2) is complex real ext-real Element of REAL

sqrt (((Re r1) ^2) + ((Im r1) ^2)) is complex real ext-real Element of REAL

(abs r0) + (abs r1) is complex real ext-real Element of REAL

((abs r0) + (abs r1)) + 1 is complex real ext-real Element of REAL

t is complex real ext-real Element of REAL

t is complex real ext-real set

abs t is complex real ext-real Element of REAL

Re t is complex real ext-real Element of REAL

(Re t) ^2 is complex real ext-real Element of REAL

(Re t) * (Re t) is complex real ext-real set

Im t is complex real ext-real Element of REAL

(Im t) ^2 is complex real ext-real Element of REAL

(Im t) * (Im t) is complex real ext-real set

((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL

sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL

t + 0 is complex real ext-real Element of REAL

- (abs r1) is complex real ext-real Element of REAL

- (abs r0) is complex real ext-real Element of REAL

(- (abs r0)) + (- (abs r1)) is complex real ext-real Element of REAL

0 + t is complex real ext-real Element of REAL

(- (abs r0)) - (abs r1) is complex real ext-real Element of REAL

- 1 is complex real ext-real non positive V48() V49() Element of INT

((- (abs r0)) - (abs r1)) + (- 1) is complex real ext-real Element of REAL

((- (abs r0)) - (abs r1)) - 1 is complex real ext-real Element of REAL

- (((abs r0) + (abs r1)) + 1) is complex real ext-real Element of REAL

r0 is complex real ext-real set

- r0 is complex real ext-real Element of REAL

r1 is ext-real set

t is complex real ext-real set

abs t is complex real ext-real Element of REAL

Re t is complex real ext-real Element of REAL

(Re t) ^2 is complex real ext-real Element of REAL

(Re t) * (Re t) is complex real ext-real set

Im t is complex real ext-real Element of REAL

(Im t) ^2 is complex real ext-real Element of REAL

(Im t) * (Im t) is complex real ext-real set

((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL

sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL

- (abs t) is complex real ext-real Element of REAL

r1 is ext-real set

t is complex real ext-real set

abs t is complex real ext-real Element of REAL

Re t is complex real ext-real Element of REAL

(Re t) ^2 is complex real ext-real Element of REAL

(Re t) * (Re t) is complex real ext-real set

Im t is complex real ext-real Element of REAL

(Im t) ^2 is complex real ext-real Element of REAL

(Im t) * (Im t) is complex real ext-real set

((Re t) ^2) + ((Im t) ^2) is complex real ext-real Element of REAL

sqrt (((Re t) ^2) + ((Im t) ^2)) is complex real ext-real Element of REAL

R is complex real ext-real set

{R} is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element set

r0 is set

R is complex-membered ext-real-membered real-membered set

r0 is complex real ext-real set

r1 is complex real ext-real set

r1 is complex-membered ext-real-membered real-membered Element of bool REAL

t is complex real ext-real set

t is complex real ext-real set

t is complex real ext-real set

t is complex real ext-real Element of REAL

m is complex real ext-real Element of REAL

m is complex real ext-real set

m - m is complex real ext-real Element of REAL

f1 is complex real ext-real set

m - (m - m) is complex real ext-real Element of REAL

(m - m) - (m - m) is complex real ext-real Element of REAL

m is complex real ext-real set

f1 is complex real ext-real set

m - f1 is complex real ext-real Element of REAL

R is complex real ext-real set

r0 is complex real ext-real set

r1 is complex-membered ext-real-membered real-membered set

R - r0 is complex real ext-real Element of REAL

R - (R - r0) is complex real ext-real Element of REAL

t is complex real ext-real set

r0 - R is complex real ext-real Element of REAL

r0 - (r0 - R) is complex real ext-real Element of REAL

t is complex real ext-real set

R is complex-membered ext-real-membered real-membered set

r0 is complex real ext-real set

r1 is complex real ext-real set

r1 is complex-membered ext-real-membered real-membered Element of bool REAL

t is complex-membered ext-real-membered real-membered Element of bool REAL

t is complex real ext-real set

m is complex real ext-real set

t is complex real ext-real set

m is complex real ext-real Element of REAL

m is complex real ext-real Element of REAL

f1 is complex real ext-real set

m + f1 is complex real ext-real Element of REAL

f2 is complex real ext-real set

(m + f1) - m is complex real ext-real Element of REAL

m - m is complex real ext-real Element of REAL

f1 is complex real ext-real set

f2 is complex real ext-real set

m + f2 is complex real ext-real Element of REAL

R is complex real ext-real set

r0 is complex real ext-real set

r1 is complex-membered ext-real-membered real-membered set

R - r0 is complex real ext-real Element of REAL

r0 + (R - r0) is complex real ext-real Element of REAL

t is complex real ext-real set

r0 - R is complex real ext-real Element of REAL

R + (r0 - R) is complex real ext-real Element of REAL

t is complex real ext-real set

R is complex-membered ext-real-membered real-membered set

r0 is complex real ext-real set

r1 is complex real ext-real set

R is complex-membered ext-real-membered real-membered set

r0 is complex real ext-real set

r1 is complex real ext-real set

R is complex real ext-real set

r0 is non empty complex-membered ext-real-membered real-membered set

(r0) is complex real ext-real set

r1 is complex real ext-real set

R + r1 is complex real ext-real Element of REAL

r1 is ext-real set

R is non empty complex-membered ext-real-membered real-membered set

(R) is complex real ext-real set

r0 is complex real ext-real set

r1 is complex real ext-real set

r0 - r1 is complex real ext-real Element of REAL

r0 + r1 is complex real ext-real Element of REAL

r1 is ext-real set

R is non empty complex-membered ext-real-membered real-membered bounded_below set

(R) is complex real ext-real set

inf R is complex real ext-real set

r0 is complex real ext-real set

r1 is ext-real set

r0 is complex real ext-real set

R is non empty complex-membered ext-real-membered real-membered bounded_above set

(R) is complex real ext-real set

sup R is complex real ext-real set

r0 is complex real ext-real set

r1 is ext-real set

r0 is complex real ext-real set

R is complex-membered ext-real-membered real-membered Element of bool REAL

(R) is complex real ext-real set

(R) is complex real ext-real set

R is complex real ext-real set

(R) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL

((R)) is complex real ext-real Element of REAL

inf (R) is complex real ext-real set

r0 is complex real ext-real set

(r0) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL

((r0)) is complex real ext-real Element of REAL

sup (r0) is complex real ext-real set

R is complex real ext-real set

(R) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL

((R)) is complex real ext-real Element of REAL

inf (R) is complex real ext-real set

((R)) is complex real ext-real Element of REAL

sup (R) is complex real ext-real set

R is complex-membered ext-real-membered real-membered Element of bool REAL

(R) is complex real ext-real Element of REAL

(R) is complex real ext-real Element of REAL

r0 is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded set

(r0) is complex real ext-real set

inf r0 is complex real ext-real set

(r0) is complex real ext-real set

sup r0 is complex real ext-real set

R is complex-membered ext-real-membered real-membered Element of bool REAL

(R) is complex real ext-real Element of REAL

(R) is complex real ext-real Element of REAL

r0 is complex real ext-real set

r1 is complex real ext-real set

r0 is complex real ext-real Element of REAL

r1 is set

t is set

(r0) is non empty trivial complex-membered ext-real-membered real-membered finite left_end right_end bounded_below bounded_above real-bounded 1 -element Element of bool REAL

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 is complex real ext-real set

r1 is complex real ext-real Element of REAL

abs r1 is complex real ext-real Element of REAL

Re r1 is complex real ext-real Element of REAL

(Re r1) ^2 is complex real ext-real Element of REAL

(Re r1) * (Re r1) is complex real ext-real set

Im r1 is complex real ext-real Element of REAL

(Im r1) ^2 is complex real ext-real Element of REAL

(Im r1) * (Im r1) is complex real ext-real set

((Re r1) ^2) + ((Im r1) ^2) is complex real ext-real Element of REAL

sqrt (((Re r1) ^2) + ((Im r1) ^2)) is complex real ext-real Element of REAL

t is complex real ext-real Element of REAL

t is complex real ext-real set

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

(abs R) . f1 is complex real ext-real Element of REAL

((abs R) . f1) - t is complex real ext-real Element of REAL

abs (((abs R) . f1) - t) is complex real ext-real Element of REAL

Re (((abs R) . f1) - t) is complex real ext-real Element of REAL

(Re (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL

(Re (((abs R) . f1) - t)) * (Re (((abs R) . f1) - t)) is complex real ext-real set

Im (((abs R) . f1) - t) is complex real ext-real Element of REAL

(Im (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL

(Im (((abs R) . f1) - t)) * (Im (((abs R) . f1) - t)) is complex real ext-real set

((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2)) is complex real ext-real Element of REAL

R . f1 is complex real ext-real Element of REAL

r1 - (R . f1) is complex real ext-real Element of REAL

abs (r1 - (R . f1)) is complex real ext-real Element of REAL

Re (r1 - (R . f1)) is complex real ext-real Element of REAL

(Re (r1 - (R . f1))) ^2 is complex real ext-real Element of REAL

(Re (r1 - (R . f1))) * (Re (r1 - (R . f1))) is complex real ext-real set

Im (r1 - (R . f1)) is complex real ext-real Element of REAL

(Im (r1 - (R . f1))) ^2 is complex real ext-real Element of REAL

(Im (r1 - (R . f1))) * (Im (r1 - (R . f1))) is complex real ext-real set

((Re (r1 - (R . f1))) ^2) + ((Im (r1 - (R . f1))) ^2) is complex real ext-real Element of REAL

sqrt (((Re (r1 - (R . f1))) ^2) + ((Im (r1 - (R . f1))) ^2)) is complex real ext-real Element of REAL

(R . f1) - r1 is complex real ext-real Element of REAL

- ((R . f1) - r1) is complex real ext-real Element of REAL

abs (- ((R . f1) - r1)) is complex real ext-real Element of REAL

Re (- ((R . f1) - r1)) is complex real ext-real Element of REAL

(Re (- ((R . f1) - r1))) ^2 is complex real ext-real Element of REAL

(Re (- ((R . f1) - r1))) * (Re (- ((R . f1) - r1))) is complex real ext-real set

Im (- ((R . f1) - r1)) is complex real ext-real Element of REAL

(Im (- ((R . f1) - r1))) ^2 is complex real ext-real Element of REAL

(Im (- ((R . f1) - r1))) * (Im (- ((R . f1) - r1))) is complex real ext-real set

((Re (- ((R . f1) - r1))) ^2) + ((Im (- ((R . f1) - r1))) ^2) is complex real ext-real Element of REAL

sqrt (((Re (- ((R . f1) - r1))) ^2) + ((Im (- ((R . f1) - r1))) ^2)) is complex real ext-real Element of REAL

abs ((R . f1) - r1) is complex real ext-real Element of REAL

Re ((R . f1) - r1) is complex real ext-real Element of REAL

(Re ((R . f1) - r1)) ^2 is complex real ext-real Element of REAL

(Re ((R . f1) - r1)) * (Re ((R . f1) - r1)) is complex real ext-real set

Im ((R . f1) - r1) is complex real ext-real Element of REAL

(Im ((R . f1) - r1)) ^2 is complex real ext-real Element of REAL

(Im ((R . f1) - r1)) * (Im ((R . f1) - r1)) is complex real ext-real set

((Re ((R . f1) - r1)) ^2) + ((Im ((R . f1) - r1)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . f1) - r1)) ^2) + ((Im ((R . f1) - r1)) ^2)) is complex real ext-real Element of REAL

abs (R . f1) is complex real ext-real Element of REAL

Re (R . f1) is complex real ext-real Element of REAL

(Re (R . f1)) ^2 is complex real ext-real Element of REAL

(Re (R . f1)) * (Re (R . f1)) is complex real ext-real set

Im (R . f1) is complex real ext-real Element of REAL

(Im (R . f1)) ^2 is complex real ext-real Element of REAL

(Im (R . f1)) * (Im (R . f1)) is complex real ext-real set

((Re (R . f1)) ^2) + ((Im (R . f1)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (R . f1)) ^2) + ((Im (R . f1)) ^2)) is complex real ext-real Element of REAL

t - (abs (R . f1)) is complex real ext-real Element of REAL

(abs (R . f1)) - t is complex real ext-real Element of REAL

- (abs ((R . f1) - r1)) is complex real ext-real Element of REAL

- (t - (abs (R . f1))) is complex real ext-real Element of REAL

abs ((abs (R . f1)) - t) is complex real ext-real Element of REAL

Re ((abs (R . f1)) - t) is complex real ext-real Element of REAL

(Re ((abs (R . f1)) - t)) ^2 is complex real ext-real Element of REAL

(Re ((abs (R . f1)) - t)) * (Re ((abs (R . f1)) - t)) is complex real ext-real set

Im ((abs (R . f1)) - t) is complex real ext-real Element of REAL

(Im ((abs (R . f1)) - t)) ^2 is complex real ext-real Element of REAL

(Im ((abs (R . f1)) - t)) * (Im ((abs (R . f1)) - t)) is complex real ext-real set

((Re ((abs (R . f1)) - t)) ^2) + ((Im ((abs (R . f1)) - t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((abs (R . f1)) - t)) ^2) + ((Im ((abs (R . f1)) - t)) ^2)) is complex real ext-real Element of REAL

(abs R) . f1 is complex real ext-real Element of REAL

((abs R) . f1) - t is complex real ext-real Element of REAL

abs (((abs R) . f1) - t) is complex real ext-real Element of REAL

Re (((abs R) . f1) - t) is complex real ext-real Element of REAL

(Re (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL

(Re (((abs R) . f1) - t)) * (Re (((abs R) . f1) - t)) is complex real ext-real set

Im (((abs R) . f1) - t) is complex real ext-real Element of REAL

(Im (((abs R) . f1) - t)) ^2 is complex real ext-real Element of REAL

(Im (((abs R) . f1) - t)) * (Im (((abs R) . f1) - t)) is complex real ext-real set

((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (((abs R) . f1) - t)) ^2) + ((Im (((abs R) . f1) - t)) ^2)) is complex real ext-real Element of REAL

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]

abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (abs R) is complex real ext-real Element of REAL

lim R is complex real ext-real Element of REAL

abs (lim R) is complex real ext-real Element of REAL

Re (lim R) is complex real ext-real Element of REAL

(Re (lim R)) ^2 is complex real ext-real Element of REAL

(Re (lim R)) * (Re (lim R)) is complex real ext-real set

Im (lim R) is complex real ext-real Element of REAL

(Im (lim R)) ^2 is complex real ext-real Element of REAL

(Im (lim R)) * (Im (lim R)) is complex real ext-real set

((Re (lim R)) ^2) + ((Im (lim R)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (lim R)) ^2) + ((Im (lim R)) ^2)) is complex real ext-real Element of REAL

r0 is complex real ext-real set

r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . t is complex real ext-real Element of REAL

(lim R) - (R . t) is complex real ext-real Element of REAL

abs ((lim R) - (R . t)) is complex real ext-real Element of REAL

Re ((lim R) - (R . t)) is complex real ext-real Element of REAL

(Re ((lim R) - (R . t))) ^2 is complex real ext-real Element of REAL

(Re ((lim R) - (R . t))) * (Re ((lim R) - (R . t))) is complex real ext-real set

Im ((lim R) - (R . t)) is complex real ext-real Element of REAL

(Im ((lim R) - (R . t))) ^2 is complex real ext-real Element of REAL

(Im ((lim R) - (R . t))) * (Im ((lim R) - (R . t))) is complex real ext-real set

((Re ((lim R) - (R . t))) ^2) + ((Im ((lim R) - (R . t))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((lim R) - (R . t))) ^2) + ((Im ((lim R) - (R . t))) ^2)) is complex real ext-real Element of REAL

(R . t) - (lim R) is complex real ext-real Element of REAL

- ((R . t) - (lim R)) is complex real ext-real Element of REAL

abs (- ((R . t) - (lim R))) is complex real ext-real Element of REAL

Re (- ((R . t) - (lim R))) is complex real ext-real Element of REAL

(Re (- ((R . t) - (lim R)))) ^2 is complex real ext-real Element of REAL

(Re (- ((R . t) - (lim R)))) * (Re (- ((R . t) - (lim R)))) is complex real ext-real set

Im (- ((R . t) - (lim R))) is complex real ext-real Element of REAL

(Im (- ((R . t) - (lim R)))) ^2 is complex real ext-real Element of REAL

(Im (- ((R . t) - (lim R)))) * (Im (- ((R . t) - (lim R)))) is complex real ext-real set

((Re (- ((R . t) - (lim R)))) ^2) + ((Im (- ((R . t) - (lim R)))) ^2) is complex real ext-real Element of REAL

sqrt (((Re (- ((R . t) - (lim R)))) ^2) + ((Im (- ((R . t) - (lim R)))) ^2)) is complex real ext-real Element of REAL

abs ((R . t) - (lim R)) is complex real ext-real Element of REAL

Re ((R . t) - (lim R)) is complex real ext-real Element of REAL

(Re ((R . t) - (lim R))) ^2 is complex real ext-real Element of REAL

(Re ((R . t) - (lim R))) * (Re ((R . t) - (lim R))) is complex real ext-real set

Im ((R . t) - (lim R)) is complex real ext-real Element of REAL

(Im ((R . t) - (lim R))) ^2 is complex real ext-real Element of REAL

(Im ((R . t) - (lim R))) * (Im ((R . t) - (lim R))) is complex real ext-real set

((Re ((R . t) - (lim R))) ^2) + ((Im ((R . t) - (lim R))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . t) - (lim R))) ^2) + ((Im ((R . t) - (lim R))) ^2)) is complex real ext-real Element of REAL

abs (R . t) is complex real ext-real Element of REAL

Re (R . t) is complex real ext-real Element of REAL

(Re (R . t)) ^2 is complex real ext-real Element of REAL

(Re (R . t)) * (Re (R . t)) is complex real ext-real set

Im (R . t) is complex real ext-real Element of REAL

(Im (R . t)) ^2 is complex real ext-real Element of REAL

(Im (R . t)) * (Im (R . t)) is complex real ext-real set

((Re (R . t)) ^2) + ((Im (R . t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (R . t)) ^2) + ((Im (R . t)) ^2)) is complex real ext-real Element of REAL

(abs (lim R)) - (abs (R . t)) is complex real ext-real Element of REAL

(abs (R . t)) - (abs (lim R)) is complex real ext-real Element of REAL

- (abs ((R . t) - (lim R))) is complex real ext-real Element of REAL

- ((abs (lim R)) - (abs (R . t))) is complex real ext-real Element of REAL

abs ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL

Re ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL

(Re ((abs (R . t)) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL

(Re ((abs (R . t)) - (abs (lim R)))) * (Re ((abs (R . t)) - (abs (lim R)))) is complex real ext-real set

Im ((abs (R . t)) - (abs (lim R))) is complex real ext-real Element of REAL

(Im ((abs (R . t)) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL

(Im ((abs (R . t)) - (abs (lim R)))) * (Im ((abs (R . t)) - (abs (lim R)))) is complex real ext-real set

((Re ((abs (R . t)) - (abs (lim R)))) ^2) + ((Im ((abs (R . t)) - (abs (lim R)))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((abs (R . t)) - (abs (lim R)))) ^2) + ((Im ((abs (R . t)) - (abs (lim R)))) ^2)) is complex real ext-real Element of REAL

(abs R) . t is complex real ext-real Element of REAL

((abs R) . t) - (abs (lim R)) is complex real ext-real Element of REAL

abs (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL

Re (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL

(Re (((abs R) . t) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL

(Re (((abs R) . t) - (abs (lim R)))) * (Re (((abs R) . t) - (abs (lim R)))) is complex real ext-real set

Im (((abs R) . t) - (abs (lim R))) is complex real ext-real Element of REAL

(Im (((abs R) . t) - (abs (lim R)))) ^2 is complex real ext-real Element of REAL

(Im (((abs R) . t) - (abs (lim R)))) * (Im (((abs R) . t) - (abs (lim R)))) is complex real ext-real set

((Re (((abs R) . t) - (abs (lim R)))) ^2) + ((Im (((abs R) . t) - (abs (lim R)))) ^2) is complex real ext-real Element of REAL

sqrt (((Re (((abs R) . t) - (abs (lim R)))) ^2) + ((Im (((abs R) . t) - (abs (lim R)))) ^2)) is complex real ext-real Element of REAL

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

abs R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (abs R) is complex real ext-real Element of REAL

lim R is complex real ext-real Element of REAL

r0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . r0 is complex real ext-real Element of REAL

abs (R . r0) is complex real ext-real Element of REAL

Re (R . r0) is complex real ext-real Element of REAL

(Re (R . r0)) ^2 is complex real ext-real Element of REAL

(Re (R . r0)) * (Re (R . r0)) is complex real ext-real set

Im (R . r0) is complex real ext-real Element of REAL

(Im (R . r0)) ^2 is complex real ext-real Element of REAL

(Im (R . r0)) * (Im (R . r0)) is complex real ext-real set

((Re (R . r0)) ^2) + ((Im (R . r0)) ^2) is complex real ext-real Element of REAL

sqrt (((Re (R . r0)) ^2) + ((Im (R . r0)) ^2)) is complex real ext-real Element of REAL

- (abs (R . r0)) is complex real ext-real Element of REAL

(abs R) . r0 is complex real ext-real Element of REAL

- ((abs R) . r0) is complex real ext-real Element of REAL

- (abs R) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

- 1 is complex real ext-real non positive set

(- 1) (#) (abs R) is Relation-like NAT -defined Function-like non empty total complex-valued ext-real-valued real-valued set

(- (abs R)) . r0 is complex real ext-real Element of REAL

lim (- (abs R)) is complex real ext-real Element of REAL

- (lim (abs R)) is complex real ext-real Element of REAL

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r1 is complex real ext-real set

t is complex real ext-real set

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . m is complex real ext-real Element of REAL

(R . m) - r1 is complex real ext-real Element of REAL

abs ((R . m) - r1) is complex real ext-real Element of REAL

Re ((R . m) - r1) is complex real ext-real Element of REAL

(Re ((R . m) - r1)) ^2 is complex real ext-real Element of REAL

(Re ((R . m) - r1)) * (Re ((R . m) - r1)) is complex real ext-real set

Im ((R . m) - r1) is complex real ext-real Element of REAL

(Im ((R . m) - r1)) ^2 is complex real ext-real Element of REAL

(Im ((R . m) - r1)) * (Im ((R . m) - r1)) is complex real ext-real set

((Re ((R . m) - r1)) ^2) + ((Im ((R . m) - r1)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . m) - r1)) ^2) + ((Im ((R . m) - r1)) ^2)) is complex real ext-real Element of REAL

f1 is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

r0 * f1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0

f1 . m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . m is complex real ext-real Element of REAL

r0 . (f1 . m) is complex real ext-real Element of REAL

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim R is complex real ext-real Element of REAL

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim r0 is complex real ext-real Element of REAL

r1 is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

r0 * r1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0

t is complex real ext-real set

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r1 . m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . m is complex real ext-real Element of REAL

r0 . (r1 . m) is complex real ext-real Element of REAL

(R . m) - (lim r0) is complex real ext-real Element of REAL

abs ((R . m) - (lim r0)) is complex real ext-real Element of REAL

Re ((R . m) - (lim r0)) is complex real ext-real Element of REAL

(Re ((R . m) - (lim r0))) ^2 is complex real ext-real Element of REAL

(Re ((R . m) - (lim r0))) * (Re ((R . m) - (lim r0))) is complex real ext-real set

Im ((R . m) - (lim r0)) is complex real ext-real Element of REAL

(Im ((R . m) - (lim r0))) ^2 is complex real ext-real Element of REAL

(Im ((R . m) - (lim r0))) * (Im ((R . m) - (lim r0))) is complex real ext-real set

((Re ((R . m) - (lim r0))) ^2) + ((Im ((R . m) - (lim r0))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . m) - (lim r0))) ^2) + ((Im ((R . m) - (lim r0))) ^2)) is complex real ext-real Element of REAL

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r1 is complex real ext-real set

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t is complex real ext-real set

m is complex real ext-real set

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . f2 is complex real ext-real Element of REAL

(R . f2) - r1 is complex real ext-real Element of REAL

abs ((R . f2) - r1) is complex real ext-real Element of REAL

Re ((R . f2) - r1) is complex real ext-real Element of REAL

(Re ((R . f2) - r1)) ^2 is complex real ext-real Element of REAL

(Re ((R . f2) - r1)) * (Re ((R . f2) - r1)) is complex real ext-real set

Im ((R . f2) - r1) is complex real ext-real Element of REAL

(Im ((R . f2) - r1)) ^2 is complex real ext-real Element of REAL

(Im ((R . f2) - r1)) * (Im ((R . f2) - r1)) is complex real ext-real set

((Re ((R . f2) - r1)) ^2) + ((Im ((R . f2) - r1)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . f2) - r1)) ^2) + ((Im ((R . f2) - r1)) ^2)) is complex real ext-real Element of REAL

r0 . f2 is complex real ext-real Element of REAL

(r0 . f2) - t is complex real ext-real Element of REAL

abs ((r0 . f2) - t) is complex real ext-real Element of REAL

Re ((r0 . f2) - t) is complex real ext-real Element of REAL

(Re ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL

(Re ((r0 . f2) - t)) * (Re ((r0 . f2) - t)) is complex real ext-real set

Im ((r0 . f2) - t) is complex real ext-real Element of REAL

(Im ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL

(Im ((r0 . f2) - t)) * (Im ((r0 . f2) - t)) is complex real ext-real set

((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2)) is complex real ext-real Element of REAL

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r0 . f2 is complex real ext-real Element of REAL

R . f2 is complex real ext-real Element of REAL

(r0 . f2) - t is complex real ext-real Element of REAL

abs ((r0 . f2) - t) is complex real ext-real Element of REAL

Re ((r0 . f2) - t) is complex real ext-real Element of REAL

(Re ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL

(Re ((r0 . f2) - t)) * (Re ((r0 . f2) - t)) is complex real ext-real set

Im ((r0 . f2) - t) is complex real ext-real Element of REAL

(Im ((r0 . f2) - t)) ^2 is complex real ext-real Element of REAL

(Im ((r0 . f2) - t)) * (Im ((r0 . f2) - t)) is complex real ext-real set

((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((r0 . f2) - t)) ^2) + ((Im ((r0 . f2) - t)) ^2)) is complex real ext-real Element of REAL

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim R is complex real ext-real Element of REAL

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim r0 is complex real ext-real Element of REAL

r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t is complex real ext-real set

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R . m is complex real ext-real Element of REAL

(R . m) - (lim R) is complex real ext-real Element of REAL

abs ((R . m) - (lim R)) is complex real ext-real Element of REAL

Re ((R . m) - (lim R)) is complex real ext-real Element of REAL

(Re ((R . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Re ((R . m) - (lim R))) * (Re ((R . m) - (lim R))) is complex real ext-real set

Im ((R . m) - (lim R)) is complex real ext-real Element of REAL

(Im ((R . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Im ((R . m) - (lim R))) * (Im ((R . m) - (lim R))) is complex real ext-real set

((Re ((R . m) - (lim R))) ^2) + ((Im ((R . m) - (lim R))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((R . m) - (lim R))) ^2) + ((Im ((R . m) - (lim R))) ^2)) is complex real ext-real Element of REAL

r0 . m is complex real ext-real Element of REAL

(r0 . m) - (lim R) is complex real ext-real Element of REAL

abs ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

Re ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

(Re ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Re ((r0 . m) - (lim R))) * (Re ((r0 . m) - (lim R))) is complex real ext-real set

Im ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

(Im ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Im ((r0 . m) - (lim R))) * (Im ((r0 . m) - (lim R))) is complex real ext-real set

((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2)) is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r0 . m is complex real ext-real Element of REAL

R . m is complex real ext-real Element of REAL

(r0 . m) - (lim R) is complex real ext-real Element of REAL

abs ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

Re ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

(Re ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Re ((r0 . m) - (lim R))) * (Re ((r0 . m) - (lim R))) is complex real ext-real set

Im ((r0 . m) - (lim R)) is complex real ext-real Element of REAL

(Im ((r0 . m) - (lim R))) ^2 is complex real ext-real Element of REAL

(Im ((r0 . m) - (lim R))) * (Im ((r0 . m) - (lim R))) is complex real ext-real set

((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((r0 . m) - (lim R))) ^2) + ((Im ((r0 . m) - (lim R))) ^2)) is complex real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

the Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:] is Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]

R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]

r0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

R ^\ r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of R

r1 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r0 ^\ R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0

lim (r0 ^\ R) is complex real ext-real Element of REAL

lim r0 is complex real ext-real Element of REAL

R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

r0 ^\ R is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of r0

r1 is complex real ext-real set

t is complex real ext-real set

t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

r0 . m is complex real ext-real Element of REAL

(r0 . m) - r1 is complex real ext-real Element of REAL

abs ((r0 . m) - r1) is complex real ext-real Element of REAL

Re ((r0 . m) - r1) is complex real ext-real Element of REAL

(Re ((r0 . m) - r1)) ^2 is complex real ext-real Element of REAL

(Re ((r0 . m) - r1)) * (Re ((r0 . m) - r1)) is complex real ext-real set

Im ((r0 . m) - r1) is complex real ext-real Element of REAL

(Im ((r0 . m) - r1)) ^2 is complex real ext-real Element of REAL

(Im ((r0 . m) - r1)) * (Im ((r0 . m) - r1)) is complex real ext-real set

((Re ((r0 . m) - r1)) ^2) + ((Im ((r0 . m) - r1)) ^2) is complex real ext-real Element of REAL

sqrt (((Re ((r0 . m) - r1)) ^2) + ((Im ((r0 . m) - r1)) ^2)) is complex real ext-real Element of REAL

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative finite cardinal set

(t + R) + f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

m - R is complex real ext-real V48() V49() Element of INT

f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

t + f2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

(t + f2) + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

- R is complex real ext-real non positive V48() V49() Element of INT

((t + f2) + R) + (- R) is complex real ext-real V48() V49() Element of INT

f1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

f1 + R is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered finite bounded_below bounded_above real-bounded cardinal Element of NAT

(r0 ^\ R) . f1 is complex real ext-real Element of REAL

((r0