:: MATRTOP1 semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

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

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

{ b

(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

{ b

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

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