REAL is non empty non trivial non finite V197() V198() V199() V203() set
NAT is non trivial ordinal non finite cardinal limit_cardinal V197() V198() V199() V200() V201() V202() V203() Element of bool REAL
bool REAL is non trivial non finite set
INT is non empty non trivial non finite V197() V198() V199() V200() V201() V203() set
K868() is strict doubleLoopStr
the carrier of K868() is set
COMPLEX is non empty non trivial non finite V197() V203() set
RAT is non empty non trivial non finite V197() V198() V199() V200() V203() set
[:COMPLEX,COMPLEX:] is Relation-like non trivial non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non trivial non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set
[:REAL,REAL:] is Relation-like non trivial non finite complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non trivial non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non trivial non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is set
NAT is non trivial ordinal non finite cardinal limit_cardinal V197() V198() V199() V200() V201() V202() V203() set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
K238() is set
1 is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
K284(NAT) is V88() set
2 is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real V30() V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() Element of NAT
K636(0,1,2) is finite V197() V198() V199() V200() V201() V202() set
[:K636(0,1,2),K636(0,1,2):] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
[:[:K636(0,1,2),K636(0,1,2):],K636(0,1,2):] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:K636(0,1,2),K636(0,1,2):],K636(0,1,2):] is finite V38() set
bool [:K636(0,1,2),K636(0,1,2):] is finite V38() set
K694() is non empty strict multMagma
the carrier of K694() is non empty set
K699() is non empty strict V141() V142() V143() V145() V227() V228() V229() V230() V231() V232() multMagma
K700() is non empty strict V143() V145() V230() V231() V232() M34(K699())
K701() is non empty strict V141() V143() V145() V230() V231() V232() V233() M37(K699(),K700())
K703() is non empty strict V141() V143() V145() multMagma
K704() is non empty strict V141() V143() V145() V233() M34(K703())
{{},1} is non empty finite V38() V197() V198() V199() V200() V201() V202() set
[:NAT,REAL:] is Relation-like non trivial non finite complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non trivial non finite set
[:1,1:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is finite V38() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is finite V38() set
[:[:1,1:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is set
[:2,2:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty TopSpace-like right_complementable V148() V149() V150() V151() V152() V153() V154() V217() V218() V287() L22()
the carrier of (TOP-REAL 2) is non empty set
3 is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V125( REAL ) V126( REAL ) complex-valued ext-real-valued real-valued V251( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
REAL 0 is functional non empty FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
TOP-REAL 0 is non empty TopSpace-like right_complementable V148() V149() V150() V151() V152() V153() V154() V217() V218() V287() L22()
0. (TOP-REAL 0) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V64( TOP-REAL 0) ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
the ZeroF of (TOP-REAL 0) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() Element of the carrier of (TOP-REAL 0)
{(0. (TOP-REAL 0))} is functional non empty trivial finite V38() 1 -element V197() V198() V199() V200() V201() V202() set
Seg 1 is non empty trivial finite 1 -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
F_Real is non empty non degenerated non trivial right_complementable almost_left_invertible strict V141() V143() V145() V148() V149() V150() right-distributive left-distributive right_unital well-unital V162() left_unital doubleLoopStr
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V125( REAL ) V126( REAL ) complex-valued ext-real-valued real-valued V251( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
doubleLoopStr(# REAL,addreal,multreal,1,0 #) is strict doubleLoopStr
the carrier of F_Real is non empty non trivial V197() V198() V199() set
- 1 is V28() real V30() V31() ext-real non positive Element of INT
addcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like total quasi_total V125( COMPLEX ) V126( COMPLEX ) complex-valued V251( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ordinal natural V28() real finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V197() V198() V199() V200() V201() V202() V203() FinSequence of REAL
Sum (<*> REAL) is V28() real ext-real Element of REAL
sqrt 0 is V28() real ext-real non negative Element of REAL
n is set
[:n,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:n,REAL:] is set
T is Relation-like non-empty n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding Element of bool [:n,REAL:]
A is set
T | A is Relation-like n -defined A -defined n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:n,REAL:]
Tn is V28() real ext-real set
rng (T | A) is V197() V198() V199() set
rng (T | A) is V197() V198() V199() Element of bool REAL
rng T is V137() V197() V198() V199() Element of bool REAL
n is set
[:n,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:n,REAL:] is set
T is Relation-like non-empty n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding Element of bool [:n,REAL:]
A is set
T | A is Relation-like n -defined A -defined n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:n,REAL:]
Tn is V28() real ext-real set
rng (T | A) is V197() V198() V199() set
rng (T | A) is V197() V198() V199() Element of bool REAL
rng T is V137() V197() V198() V199() Element of bool REAL
n is set
[:n,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:n,REAL:] is set
T is Relation-like n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding Element of bool [:n,REAL:]
A is set
T | A is Relation-like n -defined A -defined n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:n,REAL:]
Tn is V28() real ext-real set
rng (T | A) is V197() V198() V199() set
rng (T | A) is V197() V198() V199() Element of bool REAL
rng T is V197() V198() V199() Element of bool REAL
n is set
[:n,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:n,REAL:] is set
T is Relation-like n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding Element of bool [:n,REAL:]
A is set
T | A is Relation-like n -defined A -defined n -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:n,REAL:]
Tn is V28() real ext-real set
rng (T | A) is V197() V198() V199() set
rng (T | A) is V197() V198() V199() Element of bool REAL
rng T is V197() V198() V199() Element of bool REAL
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt n is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom n is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (sqrt n) is set
A is ordinal natural V28() real finite cardinal ext-real non negative set
Seg A is finite A -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= A ) } is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng n is finite V197() V198() V199() Element of bool REAL
n is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(n) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(A) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
(n) + (A) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
the addF of F_Real is Relation-like [: the carrier of F_Real, the carrier of F_Real:] -defined the carrier of F_Real -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:]
[: the carrier of F_Real, the carrier of F_Real:] is Relation-like complex-valued ext-real-valued real-valued set
[:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:] is set
K446( the carrier of F_Real, the carrier of F_Real, the carrier of F_Real, the addF of F_Real,(n),(A)) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
n + A is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
n ^ A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt (n ^ A) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(sqrt n) ^ (sqrt A) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (sqrt (n ^ A)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (n ^ A) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (sqrt A) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
len (sqrt A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
dom (sqrt n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom n is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
len (sqrt n) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
len n is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
len (sqrt (n ^ A)) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
L is ordinal natural V28() real finite cardinal ext-real non negative set
(sqrt (n ^ A)) . L is V28() real ext-real set
((sqrt n) ^ (sqrt A)) . L is V28() real ext-real set
(n ^ A) . L is V28() real ext-real set
sqrt ((n ^ A) . L) is V28() real ext-real set
n . L is V28() real ext-real set
(sqrt n) . L is V28() real ext-real set
sqrt (n . L) is V28() real ext-real set
x is ordinal natural V28() real finite cardinal ext-real non negative set
(len n) + x is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
x is ordinal natural V28() real finite cardinal ext-real non negative set
(len n) + x is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
A . x is V28() real ext-real set
(sqrt A) . x is V28() real ext-real set
sqrt (A . x) is V28() real ext-real set
len (n ^ A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(len (sqrt n)) + (len (sqrt A)) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
len ((sqrt n) ^ (sqrt A)) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
n is V28() real ext-real set
<*n*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing set
[1,n] is set
{1,n} is non empty finite V197() V198() V199() set
{1} is non empty trivial finite V38() 1 -element V197() V198() V199() V200() V201() V202() set
{{1,n},{1}} is non empty finite V38() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite 1 -element set
sqrt <*n*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt n is V28() real ext-real set
<*(sqrt n)*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing set
[1,(sqrt n)] is set
{1,(sqrt n)} is non empty finite V197() V198() V199() set
{{1,(sqrt n)},{1}} is non empty finite V38() set
{[1,(sqrt n)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*n*> . 1 is V28() real ext-real set
dom <*n*> is non empty trivial finite 1 -element V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (sqrt <*n*>) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
len <*n*> is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
len (sqrt <*n*>) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(sqrt <*n*>) . 1 is V28() real ext-real set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
n ^2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt (n ^2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
abs n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
absreal is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
n (#) absreal is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (sqrt (n ^2)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (n ^2) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (abs n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom n is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
Tn is set
n . Tn is V28() real ext-real set
Tm is V28() real ext-real Element of REAL
(n ^2) . Tn is V28() real ext-real set
Tm ^2 is V28() real ext-real Element of REAL
K97(Tm,Tm) is V28() real ext-real non negative set
(sqrt (n ^2)) . Tn is V28() real ext-real set
sqrt ((n ^2) . Tn) is V28() real ext-real set
- Tm is V28() real ext-real Element of REAL
(abs n) . Tn is V28() real ext-real set
abs Tm is V28() real ext-real Element of REAL
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum n is V28() real ext-real set
sqrt (Sum n) is V28() real ext-real set
sqrt n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqrt n) is V28() real ext-real set
A is ordinal natural V28() real finite cardinal ext-real non negative set
A + 1 is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
Tn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len Tn is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Sum Tn is V28() real ext-real set
sqrt (Sum Tn) is V28() real ext-real set
sqrt Tn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqrt Tn) is V28() real ext-real set
rng Tn is finite V197() V198() V199() Element of bool REAL
Tm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Tm | A is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg A is finite A -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= A ) } is set
Tm | (Seg A) is Relation-like NAT -defined Seg A -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
TM is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Tm . (A + 1) is V28() real ext-real set
<*(Tm . (A + 1))*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing set
[1,(Tm . (A + 1))] is set
{1,(Tm . (A + 1))} is non empty finite V197() V198() V199() set
{1} is non empty trivial finite V38() 1 -element V197() V198() V199() V200() V201() V202() set
{{1,(Tm . (A + 1))},{1}} is non empty finite V38() set
{[1,(Tm . (A + 1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
TM ^ <*(Tm . (A + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt Tm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
sqrt TM is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
sqrt <*(Tm . (A + 1))*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(sqrt TM) ^ (sqrt <*(Tm . (A + 1))*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqrt (Tm . (A + 1)) is V28() real ext-real set
<*(sqrt (Tm . (A + 1)))*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing set
[1,(sqrt (Tm . (A + 1)))] is set
{1,(sqrt (Tm . (A + 1)))} is non empty finite V197() V198() V199() set
{{1,(sqrt (Tm . (A + 1)))},{1}} is non empty finite V38() set
{[1,(sqrt (Tm . (A + 1)))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(sqrt TM) ^ <*(sqrt (Tm . (A + 1)))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqrt Tm) is V28() real ext-real set
Sum (sqrt TM) is V28() real ext-real set
(Sum (sqrt TM)) + (sqrt (Tm . (A + 1))) is V28() real ext-real Element of REAL
len TM is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Sum TM is V28() real ext-real Element of REAL
sqrt (Sum TM) is V28() real ext-real Element of REAL
Tn . (A + 1) is V28() real ext-real set
sqrt (Tn . (A + 1)) is V28() real ext-real set
(sqrt (Sum TM)) + (sqrt (Tn . (A + 1))) is V28() real ext-real Element of REAL
(Sum TM) + (Tn . (A + 1)) is V28() real ext-real Element of REAL
dom Tn is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Sum A is V28() real ext-real set
sqrt (Sum A) is V28() real ext-real set
sqrt A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqrt A) is V28() real ext-real set
dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (sqrt A) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
len (sqrt A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
len n is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Sum A is V28() real ext-real set
sqrt (Sum A) is V28() real ext-real set
sqrt A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqrt A) is V28() real ext-real set
n is Relation-like Function-like set
dom n is set
rng n is set
A is set
[:(rng n),(dom n):] is Relation-like set
bool [:(rng n),(dom n):] is set
A is Relation-like rng n -defined dom n -valued Function-like quasi_total Element of bool [:(rng n),(dom n):]
rng A is set
T is set
n | T is Relation-like Function-like set
rng (n | T) is set
dom A is set
Tm is set
A . Tm is set
n . (A . Tm) is set
Tm is set
dom (n | T) is set
TM is set
(n | T) . Tm is set
(n | T) . TM is set
n . Tm is set
n . TM is set
L is set
A . L is set
x is set
A . x is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
A is set
n - A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng n is finite V197() set
rng (n - A) is finite set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
A is set
n - A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
rng (n - A) is finite V197() set
rng n is finite V197() V198() V199() Element of bool REAL
n is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued set
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom n is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom n)) (#) n is Relation-like NAT -defined Function-like finite complex-valued set
n is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
dom n is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom n)) (#) n is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
n is set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom A),(dom A):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom A),(dom A):] is finite V38() set
A - n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (A - n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom (A - n)),(dom (A - n)):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (A - n)),(dom (A - n)):] is finite V38() set
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
T - n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Tn is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
Tn (#) A is Relation-like dom A -defined Function-like finite set
rng Tn is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
Tm is Relation-like Function-like one-to-one set
Tm " is Relation-like Function-like one-to-one set
dom (Tm ") is set
T " n is finite set
Tn .: (T " n) is finite V197() V198() V199() V200() V201() V202() set
A " n is finite set
Tn " (A " n) is finite set
Tn .: (Tn " (A " n)) is finite V197() V198() V199() V200() V201() V202() set
dom Tn is finite set
dom T is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
(dom T) \ (T " n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
(dom A) \ (A " n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
card ((dom A) \ (A " n)) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
card (dom A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
card (A " n) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(card (dom A)) - (card (A " n)) is V28() real V30() V31() ext-real Element of INT
len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Seg (len A) is finite len A -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
Sgm ((dom A) \ (A " n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
dom (Sgm ((dom A) \ (A " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
Seg (card ((dom A) \ (A " n))) is finite card ((dom A) \ (A " n)) -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= card ((dom A) \ (A " n)) ) } is set
Tm " (A " n) is set
(Tm ") .: (A " n) is finite set
Sgm ((dom T) \ (T " n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
Tn * (Sgm ((dom T) \ (T " n))) is Relation-like NAT -defined RAT -valued dom A -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,(dom A):]
[:NAT,(dom A):] is Relation-like INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,(dom A):] is set
rng (Tn * (Sgm ((dom T) \ (T " n)))) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
rng (Sgm ((dom T) \ (T " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
Tn .: (rng (Sgm ((dom T) \ (T " n)))) is finite V197() V198() V199() V200() V201() V202() set
Tn .: ((dom T) \ (T " n)) is finite V197() V198() V199() V200() V201() V202() set
Tn .: (dom Tn) is finite V197() V198() V199() V200() V201() V202() set
(Tn .: (dom Tn)) \ (Tn .: (T " n)) is finite V197() V198() V199() V200() V201() V202() Element of bool (Tn .: (dom Tn))
bool (Tn .: (dom Tn)) is finite V38() set
x is Relation-like Function-like one-to-one set
x " is Relation-like Function-like one-to-one set
dom (x ") is set
rng x is set
dom x is set
card ((dom T) \ (T " n)) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
card (dom T) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
card (T " n) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(card (dom T)) - (card (T " n)) is V28() real V30() V31() ext-real Element of INT
dom (Sgm ((dom T) \ (T " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
rng (Sgm ((dom A) \ (A " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
rng (x ") is set
(Tn * (Sgm ((dom T) \ (T " n)))) (#) (x ") is Relation-like NAT -defined Function-like finite set
rng ((Tn * (Sgm ((dom T) \ (T " n)))) (#) (x ")) is finite set
dom (Tn * (Sgm ((dom T) \ (T " n)))) is finite V197() V198() V199() V200() V201() V202() set
dom ((Tn * (Sgm ((dom T) \ (T " n)))) (#) (x ")) is finite V197() V198() V199() V200() V201() V202() set
U is Relation-like dom (A - n) -defined dom (A - n) -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (A - n)),(dom (A - n)):]
(x ") (#) x is Relation-like Function-like one-to-one set
id ((dom A) \ (A " n)) is Relation-like (dom A) \ (A " n) -defined (dom A) \ (A " n) -valued INT -valued RAT -valued Function-like one-to-one total quasi_total finite complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:((dom A) \ (A " n)),((dom A) \ (A " n)):]
[:((dom A) \ (A " n)),((dom A) \ (A " n)):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:((dom A) \ (A " n)),((dom A) \ (A " n)):] is finite V38() set
TMx is Relation-like dom (A - n) -defined dom (A - n) -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (A - n)),(dom (A - n)):]
TMx (#) x is Relation-like dom (A - n) -defined Function-like one-to-one finite set
(id ((dom A) \ (A " n))) * (Tn * (Sgm ((dom T) \ (T " n)))) is Relation-like NAT -defined INT -valued RAT -valued (dom A) \ (A " n) -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,((dom A) \ (A " n)):]
[:NAT,((dom A) \ (A " n)):] is Relation-like INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,((dom A) \ (A " n)):] is set
TMx (#) (A - n) is Relation-like dom (A - n) -defined Function-like finite set
x (#) A is Relation-like Function-like set
TMx (#) (x (#) A) is Relation-like dom (A - n) -defined Function-like finite set
(Tn * (Sgm ((dom T) \ (T " n)))) (#) A is Relation-like NAT -defined Function-like finite set
(Sgm ((dom T) \ (T " n))) (#) T is Relation-like NAT -defined Function-like finite set
n is set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom A),(dom A):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom A),(dom A):] is finite V38() set
A - n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
Sum (A - n) is V28() set
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
T - n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
Sum (T - n) is V28() set
rng (T - n) is finite V197() set
rng (A - n) is finite V197() set
TM is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
TM (#) A is Relation-like dom A -defined Function-like finite complex-valued set
dom (A - n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom (A - n)),(dom (A - n)):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (A - n)),(dom (A - n)):] is finite V38() set
L is Relation-like dom (A - n) -defined dom (A - n) -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (A - n)),(dom (A - n)):]
L (#) (A - n) is Relation-like dom (A - n) -defined Function-like finite complex-valued set
Tn is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex "**" Tn is V28() Element of COMPLEX
Tm is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex "**" Tm is V28() Element of COMPLEX
n is set
A is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom A is finite V197() V198() V199() V200() V201() V202() set
[:(dom A),(dom A):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom A),(dom A):] is finite V38() set
T is Relation-like NAT -defined Function-like finite FinSubsequence-like set
A | n is Relation-like NAT -defined n -defined NAT -defined Function-like finite FinSubsequence-like set
Seq (A | n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (A | n) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (A | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (A | n))) (#) (A | n) is Relation-like NAT -defined Function-like finite set
Tn is ordinal natural V28() real finite cardinal ext-real non negative set
Seg Tn is finite Tn -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= Tn ) } is set
Tm is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
Tm (#) A is Relation-like dom A -defined Function-like finite set
Tm " n is finite set
T | (Tm " n) is Relation-like NAT -defined Tm " n -defined NAT -defined Function-like finite FinSubsequence-like set
Seq (T | (Tm " n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (T | (Tm " n)) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (T | (Tm " n))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (T | (Tm " n)))) (#) (T | (Tm " n)) is Relation-like NAT -defined Function-like finite set
dom (Seq (T | (Tm " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):] is finite V38() set
Sgm (Tm " n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
dom Tm is finite set
Tm | (Tm " n) is Relation-like dom A -defined Tm " n -defined dom A -defined RAT -valued dom A -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
dom (Tm | (Tm " n)) is finite set
(dom A) /\ n is finite V197() V198() V199() V200() V201() V202() set
Sgm ((dom A) /\ n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
rng (Sgm ((dom A) /\ n)) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
rng Tm is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
Tm " ((dom A) /\ n) is finite set
Tm " is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
(Tm ") .: ((dom A) /\ n) is finite V197() V198() V199() V200() V201() V202() set
(Tm | (Tm " n)) * (Sgm (Tm " n)) is Relation-like NAT -defined RAT -valued dom A -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,(dom A):]
[:NAT,(dom A):] is Relation-like INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,(dom A):] is set
rng (Sgm (Tm " n)) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
rng (Tm | (Tm " n)) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
Tm .: (Tm " ((dom A) /\ n)) is finite V197() V198() V199() V200() V201() V202() set
rng ((Tm | (Tm " n)) * (Sgm (Tm " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool REAL
((Tm | (Tm " n)) * (Sgm (Tm " n))) " is Relation-like Function-like set
dom (((Tm | (Tm " n)) * (Sgm (Tm " n))) ") is set
dom (Tm ") is finite set
card ((dom A) /\ n) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
card (Tm " n) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
dom (Sgm (Tm " n)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
Seg (card ((dom A) /\ n)) is finite card ((dom A) /\ n) -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= card ((dom A) /\ n) ) } is set
dom ((Tm | (Tm " n)) * (Sgm (Tm " n))) is finite V197() V198() V199() V200() V201() V202() set
rng (((Tm | (Tm " n)) * (Sgm (Tm " n))) ") is set
(Sgm ((dom A) /\ n)) (#) (((Tm | (Tm " n)) * (Sgm (Tm " n))) ") is Relation-like NAT -defined Function-like finite set
rng ((Sgm ((dom A) /\ n)) (#) (((Tm | (Tm " n)) * (Sgm (Tm " n))) ")) is finite set
dom T is finite V197() V198() V199() V200() V201() V202() set
dom (Sgm ((dom A) /\ n)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom ((Sgm ((dom A) /\ n)) (#) (((Tm | (Tm " n)) * (Sgm (Tm " n))) ")) is finite V197() V198() V199() V200() V201() V202() set
TMx is Relation-like dom (Seq (T | (Tm " n))) -defined dom (Seq (T | (Tm " n))) -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):]
tmx is Relation-like dom (Seq (T | (Tm " n))) -defined dom (Seq (T | (Tm " n))) -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):]
((Tm | (Tm " n)) * (Sgm (Tm " n))) * tmx is Relation-like dom (Seq (T | (Tm " n))) -defined RAT -valued dom A -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (Seq (T | (Tm " n)))),(dom A):]
[:(dom (Seq (T | (Tm " n)))),(dom A):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (Seq (T | (Tm " n)))),(dom A):] is finite V38() set
(((Tm | (Tm " n)) * (Sgm (Tm " n))) ") (#) ((Tm | (Tm " n)) * (Sgm (Tm " n))) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
(Sgm ((dom A) /\ n)) (#) ((((Tm | (Tm " n)) * (Sgm (Tm " n))) ") (#) ((Tm | (Tm " n)) * (Sgm (Tm " n)))) is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued set
id ((dom A) /\ n) is Relation-like (dom A) /\ n -defined (dom A) /\ n -valued INT -valued RAT -valued Function-like one-to-one total quasi_total finite complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:((dom A) /\ n),((dom A) /\ n):]
[:((dom A) /\ n),((dom A) /\ n):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:((dom A) /\ n),((dom A) /\ n):] is finite V38() set
(id ((dom A) /\ n)) * (Sgm ((dom A) /\ n)) is Relation-like NAT -defined INT -valued RAT -valued (dom A) /\ n -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,((dom A) /\ n):]
[:NAT,((dom A) /\ n):] is Relation-like INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,((dom A) /\ n):] is set
A | ((dom A) /\ n) is Relation-like NAT -defined (dom A) /\ n -defined NAT -defined Function-like finite FinSubsequence-like set
tmx (#) (Seq (T | (Tm " n))) is Relation-like dom (Seq (T | (Tm " n))) -defined Function-like finite set
(Tm | (Tm " n)) (#) A is Relation-like dom A -defined Function-like finite set
((Tm | (Tm " n)) * (Sgm (Tm " n))) (#) A is Relation-like NAT -defined Function-like finite set
tmx (#) (((Tm | (Tm " n)) * (Sgm (Tm " n))) (#) A) is Relation-like dom (Seq (T | (Tm " n))) -defined Function-like finite set
((id ((dom A) /\ n)) * (Sgm ((dom A) /\ n))) (#) A is Relation-like NAT -defined Function-like finite set
(id ((dom A) /\ n)) (#) A is Relation-like (dom A) /\ n -defined Function-like finite set
(Sgm ((dom A) /\ n)) (#) ((id ((dom A) /\ n)) (#) A) is Relation-like NAT -defined Function-like finite set
(Sgm ((dom A) /\ n)) (#) (A | n) is Relation-like NAT -defined Function-like finite set
n is set
A is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued set
dom A is finite V197() V198() V199() V200() V201() V202() set
[:(dom A),(dom A):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom A),(dom A):] is finite V38() set
T is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued set
A | n is Relation-like NAT -defined n -defined NAT -defined Function-like finite FinSubsequence-like complex-valued set
Seq (A | n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
dom (A | n) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (A | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (A | n))) (#) (A | n) is Relation-like NAT -defined Function-like finite complex-valued set
Sum (Seq (A | n)) is V28() set
rng (Seq (A | n)) is finite V197() set
Tm is Relation-like dom A -defined dom A -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom A),(dom A):]
Tm (#) A is Relation-like dom A -defined Function-like finite complex-valued set
Tm " n is finite set
T | (Tm " n) is Relation-like NAT -defined Tm " n -defined NAT -defined Function-like finite FinSubsequence-like complex-valued set
Seq (T | (Tm " n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued set
dom (T | (Tm " n)) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (T | (Tm " n))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (T | (Tm " n)))) (#) (T | (Tm " n)) is Relation-like NAT -defined Function-like finite complex-valued set
Sum (Seq (T | (Tm " n))) is V28() set
dom (Seq (T | (Tm " n))) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
[:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):] is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):] is finite V38() set
TM is Relation-like dom (Seq (T | (Tm " n))) -defined dom (Seq (T | (Tm " n))) -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (Seq (T | (Tm " n)))),(dom (Seq (T | (Tm " n)))):]
TM (#) (Seq (T | (Tm " n))) is Relation-like dom (Seq (T | (Tm " n))) -defined Function-like finite complex-valued set
rng (Seq (T | (Tm " n))) is finite V197() set
L is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex "**" L is V28() Element of COMPLEX
Tn is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued FinSequence of COMPLEX
addcomplex "**" Tn is V28() Element of COMPLEX
n is set
A is set
T is Relation-like NAT -defined Function-like finite FinSubsequence-like set
T | A is Relation-like NAT -defined A -defined NAT -defined Function-like finite FinSubsequence-like set
Tn is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Tn Shift T is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(Tn Shift T) | n is Relation-like NAT -defined n -defined NAT -defined Function-like finite FinSubsequence-like set
Tn Shift (T | A) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom (Tn Shift (T | A)) is finite V197() V198() V199() V200() V201() V202() set
dom (T | A) is finite V197() V198() V199() V200() V201() V202() set
{ (Tn + b1) where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : b1 in dom (T | A) } is set
U is set
TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Tn + TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
dom T is finite V197() V198() V199() V200() V201() V202() set
((Tn Shift T) | n) . U is set
(Tn Shift T) . U is set
T . TMx is set
(T | A) . TMx is set
(Tn Shift (T | A)) . U is set
dom (Tn Shift T) is finite V197() V198() V199() V200() V201() V202() set
{ (Tn + b1) where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : b1 in dom T } is set
dom ((Tn Shift T) | n) is finite V197() V198() V199() V200() V201() V202() set
U is set
TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Tn + TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
U is set
TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Tn + TMx is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
n is set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
A | n is Relation-like NAT -defined n -defined NAT -defined Function-like finite FinSubsequence-like set
Seq (A | n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (A | n) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (A | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (A | n))) (#) (A | n) is Relation-like NAT -defined Function-like finite set
len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
A ^ T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(A ^ T) | n is Relation-like NAT -defined n -defined NAT -defined Function-like finite FinSubsequence-like set
Seq ((A ^ T) | n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom ((A ^ T) | n) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom ((A ^ T) | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom ((A ^ T) | n))) (#) ((A ^ T) | n) is Relation-like NAT -defined Function-like finite set
dom (A ^ T) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
n /\ (dom (A ^ T)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
len T is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
Seg (len A) is finite len A -element V137() V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
(n /\ (dom (A ^ T))) /\ (Seg (len A)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
(n /\ (dom (A ^ T))) \ (Seg (len A)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
{ b1 where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : b1 + (len A) in (n /\ (dom (A ^ T))) \ (Seg (len A)) } is set
tmx is set
X is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
X + (len A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(len A) Shift T is Relation-like NAT -defined Function-like finite FinSubsequence-like set
A \/ ((len A) Shift T) is Relation-like NAT -defined finite set
tmx is V197() V198() V199() V200() V201() V202() Element of bool NAT
T | tmx is Relation-like NAT -defined tmx -defined NAT -defined Function-like finite FinSubsequence-like set
Seq (T | tmx) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (T | tmx) is finite V197() V198() V199() V200() V201() V202() set
Sgm (dom (T | tmx)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (T | tmx))) (#) (T | tmx) is Relation-like NAT -defined Function-like finite set
(Seq (A | n)) ^ (Seq (T | tmx)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom ((len A) Shift T) is finite V197() V198() V199() V200() V201() V202() set
(n /\ (dom (A ^ T))) /\ (dom ((len A) Shift T)) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
r is set
dom T is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
{ ((len A) + b1) where b1 is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT : b1 in dom T } is set
B is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
(len A) + B is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
1 + (len A) is non empty ordinal natural V28() real V30() V31() finite cardinal ext-real positive non negative V197() V198() V199() V200() V201() V202() Element of NAT
B + (len A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
r is ordinal natural V28() real finite cardinal ext-real non negative set
r + (len A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
B is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
B + (len A) is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
A | ((n /\ (dom (A ^ T))) /\ (Seg (len A))) is Relation-like NAT -defined (n /\ (dom (A ^ T)))