:: EUCLID_7 semantic presentation

REAL is non empty non trivial non finite V126() V127() V128() V132() set

NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() Element of bool REAL

bool REAL is non empty non trivial non finite set

RAT is non empty non trivial non finite V126() V127() V128() V129() V132() set

COMPLEX is non empty non trivial non finite V126() V132() set

INT is non empty non trivial non finite V126() V127() V128() V129() V130() V132() set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

omega is non empty non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

K346() is non empty strict multMagma

the carrier of K346() is non empty set

<REAL,+> is non empty strict V97() V98() V99() V101() left-invertible right-invertible invertible left-cancelable right-cancelable V153() multMagma

addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

multMagma(# REAL,addreal #) is strict multMagma

K352() is non empty strict V99() V101() left-cancelable right-cancelable V153() SubStr of <REAL,+>

<NAT,+> is non empty strict V97() V99() V101() left-cancelable right-cancelable V153() uniquely-decomposable SubStr of K352()

<REAL,*> is non empty strict V97() V99() V101() multMagma

multreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

multMagma(# REAL,multreal #) is strict multMagma

<NAT,*> is non empty strict V97() V99() V101() uniquely-decomposable SubStr of <REAL,*>

{} is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() set

the empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() set is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() set

2 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

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

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

1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

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

bool [:1,1:] is non empty finite V39() set

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

bool [:[:1,1:],1:] is non empty finite V39() set

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

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

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

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

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

TOP-REAL 2 is non empty right_complementable constituted-Functions constituted-FinSeqs Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V197() V227() L20()

the carrier of (TOP-REAL 2) is non empty set

{{},1} is non empty finite V39() V126() V127() V128() V129() V130() V131() set

K235() is strict doubleLoopStr

the carrier of K235() is set

the carrier of K235() * is non empty functional FinSequence-membered FinSequenceSet of the carrier of K235()

REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL

K379(NAT) is V168() set

ExtREAL is non empty V127() set

0 is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of NAT

3 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

Seg 1 is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

{1} is non empty trivial finite V39() 1 -element V126() V127() V128() V129() V130() V131() set

Seg 2 is non empty finite 2 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

{1,2} is non empty finite V39() V126() V127() V128() V129() V130() V131() set

sqrt 1 is V11() V12() ext-real Element of REAL

- 1 is V11() V12() ext-real non positive Element of REAL

B is Relation-like Function-like set

n is Relation-like Function-like set

B (#) n is Relation-like Function-like set

dom (B (#) n) is set

dom B is set

dom n is set

B " (dom n) is set

(dom B) /\ (B " (dom n)) is set

B0 is set

B . B0 is set

B0 is set

B . B0 is set

n is Relation-like set

rng n is set

dom n is set

B is set

n " B is set

(rng n) /\ B is set

n " (rng n) is set

n is set

B is non empty set

[:n,B:] is Relation-like set

bool [:n,B:] is non empty set

B0 is Relation-like n -defined B -valued Function-like total quasi_total Element of bool [:n,B:]

card n is ordinal cardinal set

card B is non empty ordinal cardinal set

<*1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing FinSequence of NAT

n is set

<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

<*1*> (#) <*n*> is Relation-like NAT -defined Function-like finite set

dom <*n*> is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

rng <*1*> is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

{1} is non empty trivial finite V39() 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

dom (<*1*> (#) <*n*>) is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

dom <*1*> is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

(<*1*> (#) <*n*>) . 1 is set

<*1*> . 1 is ordinal natural V11() V12() ext-real non negative finite cardinal Element of REAL

<*n*> . (<*1*> . 1) is set

<*n*> . 1 is set

REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL

0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

<*> REAL is empty trivial proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() FinSequence of REAL

n is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of REAL 0

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

B is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

B0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

B - B0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

diffreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-yielding ext-real-valued real-valued increasing non-decreasing Element of bool [:REAL,REAL:]

compreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

K660(REAL,addreal,(id REAL),compreal) is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

diffreal .: (B,B0) is set

- B0 is Relation-like Function-like complex-yielding set

B0 (#) compreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

K38(1) is V11() V12() ext-real non positive set

K38(1) * B0 is Relation-like Function-like set

K38(1) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

multreal [;] (K38(1),(id REAL)) is set

B0 (#) (K38(1) multreal) is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

B + (- B0) is Relation-like Function-like set

B is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

(B - B0) + B is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

addreal .: ((B - B0),B) is set

((B - B0) + B) + B0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

addreal .: (((B - B0) + B),B0) is set

B + B is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

addreal .: (B,B) is set

D0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

I is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

D0 - I is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

diffreal .: (D0,I) is set

- I is Relation-like Function-like complex-yielding set

I (#) compreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

K38(1) * I is Relation-like Function-like set

I (#) (K38(1) multreal) is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

D0 + (- I) is Relation-like Function-like set

x0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

(D0 - I) + x0 is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

((D0 - I) + x0) + I is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

- I is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

D0 + (- I) is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

(D0 + (- I)) + I is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

((D0 + (- I)) + I) + x0 is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

I + (- I) is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

D0 + (I + (- I)) is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

(D0 + (I + (- I))) + x0 is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

Seg n is finite n -element V126() V127() V128() V129() V130() V131() Element of bool NAT

(Seg n) --> 0 is Relation-like Seg n -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(Seg n),{0}:]

{0} is non empty trivial functional finite V39() 1 -element V126() V127() V128() V129() V130() V131() set

[:(Seg n),{0}:] is Relation-like RAT -valued INT -valued finite complex-yielding ext-real-valued real-valued natural-valued set

bool [:(Seg n),{0}:] is non empty finite V39() set

D0 + (n |-> 0) is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

addreal .: (D0,(n |-> 0)) is set

(D0 + (n |-> 0)) + x0 is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

D0 + x0 is Relation-like NAT -defined REAL -valued Function-like complex-yielding ext-real-valued real-valued Element of bool [:NAT,REAL:]

addreal .: (D0,x0) is set

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<:n,B:> is Relation-like Function-like set

dom <:n,B:> is set

dom n is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

dom B is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

(dom n) /\ (dom B) is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

n is set

B is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

B0 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

<:B,B0:> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

[:n,n:] is Relation-like set

rng B is finite Element of bool n

bool n is non empty set

rng B0 is finite Element of bool n

[:(rng B),(rng B0):] is Relation-like finite set

rng <:B,B0:> is finite set

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

n + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

B0 is ordinal natural V11() V12() ext-real non negative finite cardinal set

n + B0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

B + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(n + 1) + B is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

len n is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

B + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

dom n is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

n . (B + 1) is V11() V12() ext-real Element of REAL

n . B is V11() V12() ext-real Element of REAL

B is ext-real set

B0 is ext-real set

D0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

D0 + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . B is V11() V12() ext-real Element of REAL

I is ordinal natural V11() V12() ext-real non negative finite cardinal set

D0 + I is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(D0 + 1) + I is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((D0 + 1) + I) is V11() V12() ext-real Element of REAL

I + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

D0 + (I + 1) is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(D0 + 1) + (I + 1) is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((D0 + 1) + (I + 1)) is V11() V12() ext-real Element of REAL

(D0 + I) + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(D0 + I) + 0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

1 + (D0 + I) is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

((D0 + 1) + I) + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . (((D0 + 1) + I) + 1) is V11() V12() ext-real Element of REAL

D0 + 0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(D0 + 1) + 0 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((D0 + 1) + 0) is V11() V12() ext-real Element of REAL

B is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

I is ordinal natural V11() V12() ext-real non negative finite cardinal set

(D0 + 1) + I is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(len n) - 0 is V11() V12() ext-real non negative Element of REAL

B - 1 is V11() V12() ext-real Element of REAL

D0 + I is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . B0 is V11() V12() ext-real Element of REAL

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

len n is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B0 is ordinal natural V11() V12() ext-real non negative finite cardinal set

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

n . B0 is V11() V12() ext-real Element of REAL

n . B is V11() V12() ext-real Element of REAL

B + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

(B + 1) + B is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((B + 1) + B) is V11() V12() ext-real Element of REAL

B + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(B + 1) + (B + 1) is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((B + 1) + (B + 1)) is V11() V12() ext-real Element of REAL

((B + 1) + B) + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . (((B + 1) + B) + 1) is V11() V12() ext-real Element of REAL

(B + 1) + 0 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((B + 1) + 0) is V11() V12() ext-real Element of REAL

B0 -' (B + 1) is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(B + 1) + (B0 -' (B + 1)) is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . ((B + 1) + (B0 -' (B + 1))) is V11() V12() ext-real Element of REAL

B0 - (B + 1) is V11() V12() ext-real Element of REAL

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

len n is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

B0 is ordinal natural V11() V12() ext-real non negative finite cardinal set

n . B is V11() V12() ext-real Element of REAL

n . B0 is V11() V12() ext-real Element of REAL

n is Relation-like NAT -defined RAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued set

len n is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . 1 is ordinal natural V11() V12() ext-real non negative V34() finite cardinal Element of REAL

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

n . B is ordinal natural V11() V12() ext-real non negative V34() finite cardinal Element of REAL

B0 is ordinal natural V11() V12() ext-real non negative finite cardinal set

n . B0 is ordinal natural V11() V12() ext-real non negative V34() finite cardinal Element of REAL

B0 + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . (B0 + 1) is ordinal natural V11() V12() ext-real non negative V34() finite cardinal Element of REAL

0 + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

n . 0 is ordinal natural V11() V12() ext-real non negative V34() finite cardinal Element of REAL

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of n is non empty set

B is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

the carrier of B is non empty set

the Mult of B is non empty Relation-like [:REAL, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of B:], the carrier of B:]

[:REAL, the carrier of B:] is non empty non trivial Relation-like non finite set

[:[:REAL, the carrier of B:], the carrier of B:] is non empty non trivial Relation-like non finite set

bool [:[:REAL, the carrier of B:], the carrier of B:] is non empty non trivial non finite set

[:REAL, the carrier of n:] is non empty non trivial Relation-like non finite set

the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial Relation-like non finite set

bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

the Mult of n | [:REAL, the carrier of n:] is Relation-like [:REAL, the carrier of n:] -defined [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

0. B is zero Element of the carrier of B

the ZeroF of B is Element of the carrier of B

0. n is zero Element of the carrier of n

the ZeroF of n is Element of the carrier of n

the addF of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

[: the carrier of B, the carrier of B:] is non empty Relation-like set

[:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty Relation-like set

bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set

the addF of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set

the addF of n || the carrier of n is set

the addF of n | [: the carrier of n, the carrier of n:] is Relation-like [: the carrier of n, the carrier of n:] -defined [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

n is set

B is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

dom B is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

[:(dom B),(dom B):] is Relation-like RAT -valued INT -valued finite complex-yielding ext-real-valued real-valued natural-valued set

bool [:(dom B),(dom B):] is non empty finite V39() set

B0 is Relation-like dom B -defined dom B -valued Function-like one-to-one total quasi_total onto bijective finite complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(dom B),(dom B):]

B * B0 is Relation-like dom B -defined n -valued Function-like finite Element of bool [:(dom B),n:]

[:(dom B),n:] is Relation-like set

bool [:(dom B),n:] is non empty set

B is Relation-like Function-like set

dom B is set

B0 " (dom B) is finite V126() V127() V128() V129() V130() V131() Element of bool (dom B)

bool (dom B) is non empty finite V39() set

rng B0 is finite V126() V127() V128() V129() V130() V131() Element of bool (dom B)

B0 " (rng B0) is finite V126() V127() V128() V129() V130() V131() Element of bool (dom B)

dom B0 is finite V126() V127() V128() V129() V130() V131() Element of bool (dom B)

B0 (#) B is Relation-like dom B -defined Function-like finite set

dom (B0 (#) B) is finite V126() V127() V128() V129() V130() V131() Element of bool (dom B)

len B is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

Seg (len B) is finite len B -element V126() V127() V128() V129() V130() V131() Element of bool NAT

rng (B * B0) is finite Element of bool n

bool n is non empty set

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

B is ordinal natural V11() V12() ext-real non negative finite cardinal set

B0 is non empty set

B is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

len B is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

Swap (B,n,B) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

(Swap (B,n,B)) . n is set

B . B is set

(Swap (B,n,B)) . B is set

B . n is set

B /. B is Element of B0

Replace (B,n,(B /. B)) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

len (Replace (B,n,(B /. B))) is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

len (Swap (B,n,B)) is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(Swap (B,n,B)) /. B is Element of B0

B /. n is Element of B0

Replace ((Replace (B,n,(B /. B))),B,(B /. n)) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

(Replace ((Replace (B,n,(B /. B))),B,(B /. n))) /. B is Element of B0

Swap (B,B,n) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

Replace (B,B,(B /. n)) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

len (Replace (B,B,(B /. n))) is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

(Swap (B,n,B)) /. n is Element of B0

Replace ((Replace (B,B,(B /. n))),n,(B /. B)) is Relation-like NAT -defined B0 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B0

(Replace ((Replace (B,B,(B /. n))),n,(B /. B))) /. n is Element of B0

[:{},{}:] is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued INT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() set

bool [:{},{}:] is non empty finite V39() set

rng {} is empty trivial proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() with_non-empty_elements Element of bool RAT

bool RAT is non empty non trivial non finite set

dom {} is empty trivial proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of bool NAT

n is empty trivial non proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of bool [:{},{}:]

{1} is non empty trivial finite V39() 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

[:{1},{1}:] is non empty Relation-like RAT -valued INT -valued finite complex-yielding ext-real-valued real-valued natural-valued set

bool [:{1},{1}:] is non empty finite V39() set

rng <*1*> is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

dom <*1*> is non empty trivial finite 1 -element V126() V127() V128() V129() V130() V131() Element of bool NAT

B is non empty Relation-like {1} -defined {1} -valued Function-like total quasi_total finite complex-yielding ext-real-valued real-valued natural-valued Element of bool [:{1},{1}:]

n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

sort_a n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V259() FinSequence of REAL

dom (sort_a n) is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

dom n is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

B is Relation-like Function-like set

dom B is set

rng B is set

B (#) n is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

B is Relation-like Function-like set

dom B is set

rng B is set

B (#) (sort_a n) is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued FinSequence of NAT

dom n is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

[:(dom n),(dom n):] is Relation-like RAT -valued INT -valued finite complex-yielding ext-real-valued real-valued natural-valued set

bool [:(dom n),(dom n):] is non empty finite V39() set

rng n is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

sort_a B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V259() FinSequence of REAL

dom (sort_a B) is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

dom B is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

B0 is Relation-like Function-like set

dom B0 is set

rng B0 is set

B0 (#) B is Relation-like REAL -valued Function-like complex-yielding ext-real-valued real-valued set

rng (sort_a B) is finite V126() V127() V128() Element of bool REAL

rng B is finite V126() V127() V128() Element of bool REAL

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued FinSequence of NAT

rng B is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

dom B is finite V126() V127() V128() V129() V130() V131() Element of bool NAT

len B is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

Seg (len B) is finite len B -element V126() V127() V128() V129() V130() V131() Element of bool NAT

D0 is ordinal natural V11() V12() ext-real non negative finite cardinal set

D0 + 1 is non empty ordinal natural V11() V12() ext-real positive non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

B . (D0 + 1) is ordinal natural V11() V12() ext-real non negative finite cardinal Element of REAL

B . D0 is ordinal natural V11() V12() ext-real non negative finite cardinal Element of REAL

D0 is Relation-like dom n -defined dom n -valued Function-like total quasi_total finite complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(dom n),(dom n):]

I is Relation-like dom n -defined dom n -valued Function-like one-to-one total quasi_total onto bijective finite complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(dom n),(dom n):]

n * I is Relation-like dom n -defined NAT -valued RAT -valued Function-like finite complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(dom n),NAT:]

[:(dom n),NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:(dom n),NAT:] is non empty set

dom I is finite V126() V127() V128() V129() V130() V131() Element of bool (dom n)

bool (dom n) is non empty finite V39() set

B is empty trivial non proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of bool [:{},{}:]

n * B is empty trivial non proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {} -defined NAT -valued RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() Element of bool [:{},NAT:]

[:{},NAT:] is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued INT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() set

bool [:{},NAT:] is non empty finite V39() set

B0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued FinSequence of NAT

n is set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

B0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|(B,B0)| is V11() V12() ext-real Element of REAL

mlt (B,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,B0) is set

Sum (mlt (B,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,B0)),addreal) is V11() V12() ext-real Element of REAL

n is set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

B0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|(B,B0)| is V11() V12() ext-real Element of REAL

mlt (B,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,B0) is set

Sum (mlt (B,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,B0)),addreal) is V11() V12() ext-real Element of REAL

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

B0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|(B,B0)| is V11() V12() ext-real Element of REAL

mlt (B,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,B0) is set

Sum (mlt (B,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,B0)),addreal) is V11() V12() ext-real Element of REAL

n is set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.B.| is V11() V12() ext-real non negative Element of REAL

sqr B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B,B) is Relation-like Function-like set

multreal .: (B,B) is set

Sum (sqr B) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B)) is V11() V12() ext-real Element of REAL

n is () set

B is () set

n \/ B is set

B0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.B0.| is V11() V12() ext-real non negative Element of REAL

sqr B0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B0 (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B0,B0) is Relation-like Function-like set

multreal .: (B0,B0) is set

Sum (sqr B0) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B0),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B0)) is V11() V12() ext-real Element of REAL

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.n.| is V11() V12() ext-real non negative Element of REAL

sqr n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

n (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (n,n) is Relation-like Function-like set

multreal .: (n,n) is set

Sum (sqr n) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr n),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr n)) is V11() V12() ext-real Element of REAL

{n} is non empty trivial functional finite V39() 1 -element set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.B.| is V11() V12() ext-real non negative Element of REAL

sqr B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B,B) is Relation-like Function-like set

multreal .: (B,B) is set

Sum (sqr B) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B)) is V11() V12() ext-real Element of REAL

n is set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.B.| is V11() V12() ext-real non negative Element of REAL

sqr B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B,B) is Relation-like Function-like set

multreal .: (B,B) is set

Sum (sqr B) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B)) is V11() V12() ext-real Element of REAL

{B} is non empty trivial functional finite V39() 1 -element set

n \/ {B} is non empty set

n is set

n is set

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

{<*1*>} is non empty trivial functional finite V39() 1 -element Element of bool (bool [:NAT,NAT:])

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

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

B0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|(B,B0)| is V11() V12() ext-real Element of REAL

mlt (B,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,B0) is set

Sum (mlt (B,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,B0)),addreal) is V11() V12() ext-real Element of REAL

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.B.| is V11() V12() ext-real non negative Element of REAL

sqr B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B,B) is Relation-like Function-like set

multreal .: (B,B) is set

Sum (sqr B) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B)) is V11() V12() ext-real Element of REAL

1 ^2 is V11() V12() ext-real Element of REAL

K37(1,1) is ordinal natural V11() V12() ext-real non negative finite cardinal set

<*(1 ^2)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

bool (REAL n) is non empty set

{} (REAL n) is empty trivial proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () Element of bool (REAL n)

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

bool (REAL n) is non empty set

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

bool (REAL n) is non empty set

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

bool (REAL n) is non empty set

B is functional FinSequence-membered Element of bool (REAL n)

B is functional FinSequence-membered Element of bool (REAL n)

bool (REAL 0) is non empty set

n is functional FinSequence-membered Element of bool (REAL 0)

the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of n

B0 is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () Element of REAL 0

len B0 is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () Element of NAT

0* (len B0) is Relation-like NAT -defined REAL -valued Function-like finite len B0 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL (len B0)

REAL (len B0) is non empty functional FinSequence-membered FinSequenceSet of REAL

(len B0) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

(len B0) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite len B0 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of (len B0) -tuples_on REAL

Seg (len B0) is empty trivial proper ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal len B0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () Element of bool NAT

(Seg (len B0)) --> 0 is empty trivial non proper ordinal T-Sequence-like natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding Seg (len B0) -defined RAT -valued INT -valued {0} -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () Element of bool [:(Seg (len B0)),{0}:]

{0} is non empty trivial functional finite V39() 1 -element V126() V127() V128() V129() V130() V131() set

[:(Seg (len B0)),{0}:] is empty trivial ordinal natural V11() V12() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued INT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V126() V127() V128() V129() V130() V131() V132() () () () set

bool [:(Seg (len B0)),{0}:] is non empty finite V39() set

|((0* (len B0)),(0* (len B0)))| is V11() V12() ext-real Element of REAL

mlt ((0* (len B0)),(0* (len B0))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: ((0* (len B0)),(0* (len B0))) is set

Sum (mlt ((0* (len B0)),(0* (len B0)))) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt ((0* (len B0)),(0* (len B0)))),addreal) is V11() V12() ext-real Element of REAL

|.(0* (len B0)).| is V11() V12() ext-real non negative Element of REAL

sqr (0* (len B0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(0* (len B0)) (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt ((0* (len B0)),(0* (len B0))) is Relation-like Function-like set

Sum (sqr (0* (len B0))) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr (0* (len B0))),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr (0* (len B0)))) is V11() V12() ext-real Element of REAL

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

bool (REAL n) is non empty set

0* n is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

Seg n is finite n -element V126() V127() V128() V129() V130() V131() Element of bool NAT

(Seg n) --> 0 is Relation-like Seg n -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued natural-valued Element of bool [:(Seg n),{0}:]

{0} is non empty trivial functional finite V39() 1 -element V126() V127() V128() V129() V130() V131() set

[:(Seg n),{0}:] is Relation-like RAT -valued INT -valued finite complex-yielding ext-real-valued real-valued natural-valued set

bool [:(Seg n),{0}:] is non empty finite V39() set

B is functional FinSequence-membered Element of bool (REAL n)

B0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

|.B0.| is V11() V12() ext-real non negative Element of REAL

sqr B0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B0 (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B0,B0) is Relation-like Function-like set

multreal .: (B0,B0) is set

Sum (sqr B0) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B0),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B0)) is V11() V12() ext-real Element of REAL

1 / |.B0.| is V11() V12() ext-real non negative Element of REAL

(1 / |.B0.|) * B0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

(1 / |.B0.|) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [:REAL,REAL:]

id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-yielding ext-real-valued real-valued increasing non-decreasing Element of bool [:REAL,REAL:]

multreal [;] ((1 / |.B0.|),(id REAL)) is set

B0 (#) ((1 / |.B0.|) multreal) is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

B is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

{B} is non empty trivial functional finite V39() 1 -element FinSequence-membered Element of bool (REAL n)

B \/ {B} is non empty functional FinSequence-membered Element of bool (REAL n)

D0 is functional FinSequence-membered Element of bool (REAL n)

len B0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

x0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|(I,x0)| is V11() V12() ext-real Element of REAL

mlt (I,x0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (I,x0) is set

Sum (mlt (I,x0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (I,x0)),addreal) is V11() V12() ext-real Element of REAL

p is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

len p is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

z0 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of REAL n

len z0 is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

|(I,B0)| is V11() V12() ext-real Element of REAL

mlt (I,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (I,B0) is set

Sum (mlt (I,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (I,B0)),addreal) is V11() V12() ext-real Element of REAL

(1 / |.B0.|) * |(I,B0)| is V11() V12() ext-real Element of REAL

|(x0,B0)| is V11() V12() ext-real Element of REAL

mlt (x0,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (x0,B0) is set

Sum (mlt (x0,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (x0,B0)),addreal) is V11() V12() ext-real Element of REAL

(1 / |.B0.|) * |(x0,B0)| is V11() V12() ext-real Element of REAL

|(p,((1 / |.B0.|) * B0))| is V11() V12() ext-real Element of REAL

mlt (p,((1 / |.B0.|) * B0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (p,((1 / |.B0.|) * B0)) is set

Sum (mlt (p,((1 / |.B0.|) * B0))) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (p,((1 / |.B0.|) * B0))),addreal) is V11() V12() ext-real Element of REAL

|.B.| is V11() V12() ext-real non negative Element of REAL

sqr B is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

B (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (B,B) is Relation-like Function-like set

multreal .: (B,B) is set

Sum (sqr B) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr B),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr B)) is V11() V12() ext-real Element of REAL

abs (1 / |.B0.|) is V11() V12() ext-real Element of REAL

(abs (1 / |.B0.|)) * |.B0.| is V11() V12() ext-real Element of REAL

(1 / |.B0.|) * |.B0.| is V11() V12() ext-real non negative Element of REAL

I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued set

|.I.| is V11() V12() ext-real non negative Element of REAL

sqr I is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

I (#) sqrreal is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding ext-real-valued real-valued set

mlt (I,I) is Relation-like Function-like set

multreal .: (I,I) is set

Sum (sqr I) is V11() V12() ext-real Element of REAL

K608(REAL,(sqr I),addreal) is V11() V12() ext-real Element of REAL

sqrt (Sum (sqr I)) is V11() V12() ext-real Element of REAL

len B is ordinal natural V11() V12() ext-real non negative V33() V34() finite cardinal V126() V127() V128() V129() V130() V131() Element of NAT

|(B,B0)| is V11() V12() ext-real Element of REAL

mlt (B,B0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,B0) is set

Sum (mlt (B,B0)) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,B0)),addreal) is V11() V12() ext-real Element of REAL

(1 / |.B0.|) * |(B,B0)| is V11() V12() ext-real Element of REAL

|(B,((1 / |.B0.|) * B0))| is V11() V12() ext-real Element of REAL

mlt (B,((1 / |.B0.|) * B0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

multreal .: (B,((1 / |.B0.|) * B0)) is set

Sum (mlt (B,((1 / |.B0.|) * B0))) is V11() V12() ext-real Element of REAL

K608(REAL,(mlt (B,((1 / |.B0.|) * B0))),addreal) is V11() V12() ext-real Element of REAL

n is ordinal natural V11() V12() ext-real non negative finite cardinal set

REAL n is non empty functional