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

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

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite 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

K636(0,1,2) is finite V197() V198() V199() V200() V201() V202() 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

bool is non trivial non finite set

bool [:1,1:] is finite V38() set

bool [:[:1,1:],1:] is finite V38() set

bool [:[:1,1:],REAL:] is 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 () 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

TOP-REAL 0 is non empty TopSpace-like right_complementable V148() V149() V150() V151() V152() V153() V154() V217() V218() V287() L22()

the carrier of () is non empty set

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

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

Sum () is V28() real ext-real Element of REAL

n is set

bool [:n,REAL:] is set

A is set

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

bool [:n,REAL:] is set

A is set

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

bool [:n,REAL:] is set

A is set

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

bool [:n,REAL:] is set

A is set

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

dom n is finite V197() V198() V199() V200() V201() V202() Element of bool NAT
dom (sqrt n) is 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

rng n is finite V197() V198() V199() Element of bool 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:], 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

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

(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

(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

(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

[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,(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

<*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 () 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 () is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT
() . 1 is V28() real ext-real 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

sqrt (Sum n) is V28() real ext-real set

Sum (sqrt n) is V28() real ext-real 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

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

Sum (sqrt Tn) is V28() real ext-real set
rng Tn is finite V197() V198() V199() Element of bool 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 . (A + 1) is V28() real ext-real 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

sqrt (Tm . (A + 1)) is V28() real ext-real 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

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

len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT

sqrt (Sum A) is V28() real ext-real 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

len A is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT

sqrt (Sum A) is V28() real ext-real set

Sum (sqrt A) is V28() real ext-real 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

rng A is set
T is 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

A is set

rng n is finite V197() set
rng (n - A) is finite set

A is set

rng (n - A) is finite V197() set
rng n is finite V197() V198() V199() Element of bool REAL

dom n is finite V197() V198() V199() V200() V201() V202() set

dom n is finite V197() V198() V199() V200() V201() V202() set

n is set

dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT

bool [:(dom A),(dom A):] is finite V38() set

dom (A - n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT

bool [:(dom (A - n)),(dom (A - n)):] is finite V38() set

rng Tn is finite V197() V198() V199() V200() V201() V202() Element of bool REAL

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

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

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

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

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

(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)):]

bool [:NAT,((dom A) \ (A " n)):] is set
TMx (#) (A - n) is Relation-like dom (A - n) -defined Function-like finite 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

dom A is finite V197() V198() V199() V200() V201() V202() Element of bool NAT

bool [:(dom A),(dom A):] is finite V38() set

Sum (A - n) is V28() set

Sum (T - n) is V28() set
rng (T - n) is finite V197() set
rng (A - n) is finite V197() set

dom (A - n) is finite V197() V198() V199() V200() V201() V202() Element of bool NAT

bool [:(dom (A - n)),(dom (A - n)):] is finite V38() set

addcomplex "**" Tn is V28() Element of COMPLEX

addcomplex "**" Tm is V28() Element of COMPLEX
n is set

dom A is finite V197() V198() V199() V200() V201() V202() set

bool [:(dom A),(dom A):] is finite V38() set

dom (A | n) is finite V197() V198() V199() V200() V201() V202() set

(Sgm (dom (A | n))) (#) (A | n) is Relation-like NAT -defined Function-like finite 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 " n is finite set

dom (T | (Tm " n)) is finite V197() V198() V199() V200() V201() V202() set

(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

dom Tm is finite set

dom (Tm | (Tm " n)) is finite set
(dom A) /\ n is finite V197() V198() V199() V200() V201() V202() set

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 ") .: ((dom A) /\ n) is finite V197() V198() V199() V200() V201() V202() 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):]

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

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

bool [:NAT,((dom A) /\ n):] is 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

dom A is finite V197() V198() V199() V200() V201() V202() set

bool [:(dom A),(dom A):] is finite V38() set

dom (A | n) is finite V197() V198() V199() V200() V201() V202() set

(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 " n is finite set

dom (T | (Tm " n)) is finite V197() V198() V199() V200() V201() V202() set

(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

addcomplex "**" Tn is V28() Element of COMPLEX
n is set
A is set

Tn is ordinal natural V28() real V30() V31() finite cardinal ext-real non negative V197() V198() V199() V200() V201() V202() Element of NAT

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

dom (A | n) is finite V197() V198() V199() V200() V201() V202() set

(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

dom ((A ^ T) | n) is finite V197() V198() V199() V200() V201() V202() set

(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

A \/ ((len A) Shift T) is Relation-like NAT -defined finite set
tmx is V197() V198() V199() V200() V201() V202() Element of bool NAT

dom (T | tmx) is finite V197() V198() V199() V200() V201() V202() set

(Sgm (dom (T | tmx))) (#) (T | tmx) is Relation-like NAT -defined Function-like finite 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 + (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)))