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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 0 } is set
<*> 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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is 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
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len B0 } is set
(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
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