:: MATRTOP3 semantic presentation

REAL is non empty non trivial V36() V155() V156() V157() V161() set
NAT is non trivial ordinal V36() cardinal limit_cardinal V155() V156() V157() V158() V159() V160() V161() Element of bool REAL
bool REAL is non empty non trivial V36() set
COMPLEX is non empty non trivial V36() V155() V161() set
omega is non trivial ordinal V36() cardinal limit_cardinal V155() V156() V157() V158() V159() V160() V161() set
bool omega is non empty non trivial V36() set
K214() is TopStruct
the carrier of K214() is set
bool NAT is non empty non trivial V36() set
RAT is non empty non trivial V36() V155() V156() V157() V158() V161() set
INT is non empty non trivial V36() V155() V156() V157() V158() V159() V161() set
[:REAL,REAL:] is non empty non trivial Relation-like V36() complex-yielding ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty non trivial V36() set
K375() is non empty strict multMagma
the carrier of K375() is non empty set
<REAL,+> is non empty strict unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V182() multMagma
K381() is non empty strict associative commutative left-cancelable right-cancelable V182() SubStr of <REAL,+>
<NAT,+> is non empty strict unital associative commutative left-cancelable right-cancelable V182() uniquely-decomposable SubStr of K381()
<REAL,*> is non empty strict unital associative commutative multMagma
<NAT,*> is non empty strict unital associative commutative uniquely-decomposable SubStr of <REAL,*>
{} is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() set
2 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
1 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
[:1,1:] is non empty Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty V36() V40() set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty V36() V40() set
[:[:1,1:],REAL:] is non empty non trivial Relation-like V36() complex-yielding ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty non trivial V36() set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like V36() complex-yielding ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial V36() set
[:2,2:] is non empty Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is non empty non trivial Relation-like V36() complex-yielding ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty non trivial V36() set
TOP-REAL 2 is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL 2) is non empty set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like V36() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty non trivial V36() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like V36() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V36() set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued V36() complex-yielding ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial V36() set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued V36() complex-yielding ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial V36() set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial V36() set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial V36() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty set
K610() is set
0 is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element V85() V86() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() Element of NAT
K74(0,1,2) is non empty V36() V155() V156() V157() V158() V159() V160() set
[:K74(0,1,2),K74(0,1,2):] is non empty Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
[:[:K74(0,1,2),K74(0,1,2):],K74(0,1,2):] is non empty Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
bool [:[:K74(0,1,2),K74(0,1,2):],K74(0,1,2):] is non empty V36() V40() set
bool [:K74(0,1,2),K74(0,1,2):] is non empty V36() V40() set
F_Real is non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital V136() left_unital V189() V190() V191() doubleLoopStr
K560() 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:]
K562() 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:]
doubleLoopStr(# REAL,K560(),K562(),1,0 #) is strict doubleLoopStr
the carrier of F_Real is non empty non trivial V155() V156() V157() set
{{},1} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
K886() is set
bool K886() is non empty set
K887() is Element of bool K886()
[:NAT,REAL:] is non trivial Relation-like V36() complex-yielding ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial V36() set
[:NAT,COMPLEX:] is non trivial Relation-like V36() complex-yielding set
bool [:NAT,COMPLEX:] is non empty non trivial V36() set
K400(NAT) is V187() set
the carrier of F_Real * is non empty functional FinSequence-membered FinSequenceSet of the carrier of F_Real
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
3 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
TOP-REAL 0 is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
0. (TOP-REAL 0) is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() V37() V40() cardinal 0 -element V61( TOP-REAL 0) V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
the ZeroF of (TOP-REAL 0) is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() V37() V40() cardinal 0 -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() Element of the carrier of (TOP-REAL 0)
{(0. (TOP-REAL 0))} is non empty trivial functional V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
- 1 is non empty V11() real ext-real non positive negative V85() set
Seg 1 is non empty trivial V16() V36() 1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
Seg 2 is non empty V16() V36() 2 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
[1,1] is set
{1,1} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{{1,1},{1}} is non empty V36() V40() set
[1,2] is set
{{1,2},{1}} is non empty V36() V40() set
[2,1] is set
{2,1} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{2} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{2,1},{2}} is non empty V36() V40() set
[2,2] is set
{2,2} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{{2,2},{2}} is non empty V36() V40() set
0. F_Real is V11() real ext-real V61( F_Real ) Element of the carrier of F_Real
the ZeroF of F_Real is V11() real ext-real Element of the carrier of F_Real
sin 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:]
cos 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:]
cos 0 is V11() real ext-real Element of REAL
sin 0 is V11() real ext-real Element of REAL
PI is V11() real ext-real Element of REAL
2 * PI is V11() real ext-real Element of REAL
PI / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
PI * (2 ") is V11() real ext-real set
- (PI / 2) is V11() real ext-real Element of REAL
[.(- (PI / 2)),(PI / 2).] is V155() V156() V157() Element of bool REAL
K196(REAL,REAL,sin,[.(- (PI / 2)),(PI / 2).]) is V155() V156() V157() Element of bool REAL
- 1 is non empty V11() real ext-real non positive negative V85() Element of REAL
[.(- 1),1.] is V155() V156() V157() Element of bool REAL
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
Seg n is V16() V36() n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
bool [:(Seg n),(Seg n):] is non empty V36() V40() set
p is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V136() left_unital V189() V190() V191() doubleLoopStr
the carrier of p is non empty non trivial set
the carrier of p * is non empty functional FinSequence-membered FinSequenceSet of the carrier of p
q is Relation-like NAT -defined the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
Det q is Element of the carrier of p
Indices q is set
TR is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V36() complex-yielding ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg n),(Seg n):]
q * TR is Relation-like NAT -defined Seg n -defined the carrier of p * -valued the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
(q * TR) @ is Relation-like NAT -defined the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
((q * TR) @) * TR is Relation-like NAT -defined Seg n -defined the carrier of p * -valued the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
(((q * TR) @) * TR) @ is Relation-like NAT -defined the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
Det ((((q * TR) @) * TR) @) is Element of the carrier of p
Permutations n is non empty permutational set
len (Permutations n) is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
Seg (len (Permutations n)) is V16() V36() len (Permutations n) -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
- (Det q) is Element of the carrier of p
- (- (Det q)) is Element of the carrier of p
n1 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V36() complex-yielding ext-real-valued real-valued natural-valued finite-support Element of Permutations n
- ((Det q),n1) is Element of the carrier of p
Det (((q * TR) @) * TR) is Element of the carrier of p
Det ((q * TR) @) is Element of the carrier of p
- ((Det ((q * TR) @)),n1) is Element of the carrier of p
Det (q * TR) is Element of the carrier of p
- ((Det (q * TR)),n1) is Element of the carrier of p
- ((- ((Det q),n1)),n1) is Element of the carrier of p
f is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TR . f is ordinal natural V11() real ext-real non negative V36() cardinal V85() Element of REAL
X is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
[f,X] is set
{f,X} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{f} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{f,X},{f}} is non empty V36() V40() set
((((q * TR) @) * TR) @) * (f,X) is Element of the carrier of p
TR . X is ordinal natural V11() real ext-real non negative V36() cardinal V85() Element of REAL
q * ((TR . f),(TR . X)) is Element of the carrier of p
Indices ((((q * TR) @) * TR) @) is set
[X,f] is set
{X,f} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{X} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{X,f},{X}} is non empty V36() V40() set
Indices (((q * TR) @) * TR) is set
(((q * TR) @) * TR) * (X,f) is Element of the carrier of p
Indices ((q * TR) @) is set
[f,(TR . X)] is set
{f,(TR . X)} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{{f,(TR . X)},{f}} is non empty V36() V40() set
Indices (q * TR) is set
z is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
[z,f] is set
{z,f} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{z} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{z,f},{z}} is non empty V36() V40() set
((q * TR) @) * (z,f) is Element of the carrier of p
(q * TR) * (f,(TR . X)) is Element of the carrier of p
z is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
[z,f] is set
{z,f} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{z} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{z,f},{z}} is non empty V36() V40() set
((q * TR) @) * (z,f) is Element of the carrier of p
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
p is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V136() left_unital V189() V190() V191() doubleLoopStr
the carrier of p is non empty non trivial set
the carrier of p * is non empty functional FinSequence-membered FinSequenceSet of the carrier of p
q is Relation-like NAT -defined the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular diagonal upper_triangular lower_triangular Matrix of n,n, the carrier of p
q @ is Relation-like NAT -defined the carrier of p * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of p
Indices q is set
TR is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
n1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
[TR,n1] is set
{TR,n1} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{TR} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{TR,n1},{TR}} is non empty V36() V40() set
q * (TR,n1) is Element of the carrier of p
(q @) * (TR,n1) is Element of the carrier of p
[n1,TR] is set
{n1,TR} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{n1} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{n1,TR},{n1}} is non empty V36() V40() set
q * (n1,TR) is Element of the carrier of p
0. p is V61(p) Element of the carrier of p
the ZeroF of p is Element of the carrier of p
n is V11() real ext-real set
n ^2 is V11() real ext-real set
n * n is V11() real ext-real set
p is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
dom p is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT
sqr p is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
Sum (sqr p) is V11() real ext-real Element of REAL
q is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
p +* (q,n) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
sqr (p +* (q,n)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
Sum (sqr (p +* (q,n))) is V11() real ext-real Element of REAL
p . q is V11() real ext-real Element of REAL
(p . q) ^2 is V11() real ext-real Element of REAL
(p . q) * (p . q) is V11() real ext-real set
(Sum (sqr p)) - ((p . q) ^2) is V11() real ext-real Element of REAL
- ((p . q) ^2) is V11() real ext-real set
(Sum (sqr p)) + (- ((p . q) ^2)) is V11() real ext-real set
((Sum (sqr p)) - ((p . q) ^2)) + (n ^2) is V11() real ext-real Element of REAL
@ p is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
@ (@ p) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
q -' 1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
(@ (@ p)) | (q -' 1) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
Seg (q -' 1) is V16() V36() q -' 1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= q -' 1 ) } is set
(@ (@ p)) | (Seg (q -' 1)) is Relation-like NAT -defined Seg (q -' 1) -defined NAT -defined REAL -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
(@ (@ p)) /^ q is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
TR is V11() real ext-real Element of REAL
<*TR*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
[1,TR] is set
{1,TR} is non empty V36() V155() V156() V157() set
{{1,TR},{1}} is non empty V36() V40() set
{[1,TR]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
sqr <*TR*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
TR ^2 is V11() real ext-real Element of REAL
TR * TR is V11() real ext-real set
<*(TR ^2)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
[1,(TR ^2)] is set
{1,(TR ^2)} is non empty V36() V155() V156() V157() set
{{1,(TR ^2)},{1}} is non empty V36() V40() set
{[1,(TR ^2)]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
(@ (@ p)) +* (q,TR) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
((@ (@ p)) | (q -' 1)) ^ <*TR*> is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
(((@ (@ p)) | (q -' 1)) ^ <*TR*>) ^ ((@ (@ p)) /^ q) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
sqr (@ (@ p)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
sqr (((@ (@ p)) | (q -' 1)) ^ <*TR*>) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
sqr ((@ (@ p)) /^ q) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(sqr (((@ (@ p)) | (q -' 1)) ^ <*TR*>)) ^ (sqr ((@ (@ p)) /^ q)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
sqr ((@ (@ p)) | (q -' 1)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*TR*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*TR*>)) ^ (sqr ((@ (@ p)) /^ q)) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
Sum (sqr (@ (@ p))) is V11() real ext-real Element of REAL
Sum ((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*TR*>)) is V11() real ext-real Element of REAL
Sum (sqr ((@ (@ p)) /^ q)) is V11() real ext-real Element of REAL
(Sum ((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*TR*>))) + (Sum (sqr ((@ (@ p)) /^ q))) is V11() real ext-real Element of REAL
Sum (sqr ((@ (@ p)) | (q -' 1))) is V11() real ext-real Element of REAL
(Sum (sqr ((@ (@ p)) | (q -' 1)))) + (TR ^2) is V11() real ext-real Element of REAL
((Sum (sqr ((@ (@ p)) | (q -' 1)))) + (TR ^2)) + (Sum (sqr ((@ (@ p)) /^ q))) is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
<*z*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
[1,z] is set
{1,z} is non empty V36() V155() V156() V157() set
{{1,z},{1}} is non empty V36() V40() set
{[1,z]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
sqr <*z*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
z ^2 is V11() real ext-real Element of REAL
z * z is V11() real ext-real set
<*(z ^2)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
[1,(z ^2)] is set
{1,(z ^2)} is non empty V36() V155() V156() V157() set
{{1,(z ^2)},{1}} is non empty V36() V40() set
{[1,(z ^2)]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
(@ (@ p)) +* (q,z) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
((@ (@ p)) | (q -' 1)) ^ <*z*> is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
(((@ (@ p)) | (q -' 1)) ^ <*z*>) ^ ((@ (@ p)) /^ q) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
sqr ((@ (@ p)) +* (q,z)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
sqr (((@ (@ p)) | (q -' 1)) ^ <*z*>) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(sqr (((@ (@ p)) | (q -' 1)) ^ <*z*>)) ^ (sqr ((@ (@ p)) /^ q)) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
(sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*z*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*z*>)) ^ (sqr ((@ (@ p)) /^ q)) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of REAL *
Sum (sqr ((@ (@ p)) +* (q,z))) is V11() real ext-real Element of REAL
Sum ((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*z*>)) is V11() real ext-real Element of REAL
(Sum ((sqr ((@ (@ p)) | (q -' 1))) ^ (sqr <*z*>))) + (Sum (sqr ((@ (@ p)) /^ q))) is V11() real ext-real Element of REAL
(Sum (sqr ((@ (@ p)) | (q -' 1)))) + (z ^2) is V11() real ext-real Element of REAL
((Sum (sqr ((@ (@ p)) | (q -' 1)))) + (z ^2)) + (Sum (sqr ((@ (@ p)) /^ q))) is V11() real ext-real Element of REAL
n is set
p is Relation-like Function-like Function-yielding V235() set
dom p is set
q is Relation-like Function-like set
p . q is Relation-like Function-like set
TR is set
(p . q) . TR is set
q . TR is set
n is set
bool n is non empty set
p is Element of bool n
q is Relation-like Function-like Function-yielding V235() set
TR is Relation-like Function-like set
dom q is set
q . TR is Relation-like Function-like set
n1 is set
(q . TR) . n1 is set
TR . n1 is set
n is set
p is set
n /\ p is set
q is Relation-like Function-like Function-yielding V235() set
TR is Relation-like Function-like set
dom q is set
q . TR is Relation-like Function-like set
n1 is set
(q . TR) . n1 is set
TR . n1 is set
n \/ p is set
TR is Relation-like Function-like Function-yielding V235() (p) set
q is Relation-like Function-like Function-yielding V235() (n) set
TR (#) q is Relation-like Function-like Function-yielding V235() set
f is Relation-like Function-like set
dom (TR (#) q) is set
(TR (#) q) . f is Relation-like Function-like set
X is set
((TR (#) q) . f) . X is set
f . X is set
dom TR is set
TR . f is Relation-like Function-like set
(TR . f) . X is set
q . (TR . f) is Relation-like Function-like set
dom q is set
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TOP-REAL n is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty set
p is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
TOP-REAL p is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL p) is non empty set
[: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):] is non empty set
the non empty Relation-like the carrier of (TOP-REAL p) -defined the carrier of (TOP-REAL p) -valued Function-like total quasi_total homogeneous Element of bool [: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):] is non empty Relation-like the carrier of (TOP-REAL p) -defined the carrier of (TOP-REAL p) -valued Function-like total quasi_total homogeneous Element of bool [: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):]
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TOP-REAL n is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL n) is non empty set
p is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TOP-REAL p is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL p) is non empty set
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):] is non empty set
q is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL p) -valued Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):]
TR is set
dom q is non empty set
rng q is non empty set
q . TR is set
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
p is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TOP-REAL n is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
TOP-REAL p is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
q is Relation-like NAT -defined the carrier of F_Real * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,p, the carrier of F_Real
Mx2Tran q is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL p) -valued Function-like total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):]
the carrier of (TOP-REAL n) is non empty set
the carrier of (TOP-REAL p) is non empty set
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL p):] is non empty set
TR is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
TR + n1 is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is non empty Relation-like [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty Relation-like set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty Relation-like set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty set
the addF of (TOP-REAL n) . (TR,n1) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
TR + n1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(Mx2Tran q) . (TR + n1) is Relation-like NAT -defined Function-like V36() p -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL p)
(Mx2Tran q) . TR is Relation-like NAT -defined Function-like V36() p -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL p)
(Mx2Tran q) . n1 is Relation-like NAT -defined Function-like V36() p -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL p)
((Mx2Tran q) . TR) + ((Mx2Tran q) . n1) is Relation-like NAT -defined Function-like V36() p -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL p)
the addF of (TOP-REAL p) is non empty Relation-like [: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):] -defined the carrier of (TOP-REAL p) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):], the carrier of (TOP-REAL p):]
[: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):] is non empty Relation-like set
[:[: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):], the carrier of (TOP-REAL p):] is non empty Relation-like set
bool [:[: the carrier of (TOP-REAL p), the carrier of (TOP-REAL p):], the carrier of (TOP-REAL p):] is non empty set
the addF of (TOP-REAL p) . (((Mx2Tran q) . TR),((Mx2Tran q) . n1)) is Relation-like NAT -defined Function-like V36() p -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL p)
((Mx2Tran q) . TR) + ((Mx2Tran q) . n1) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
p is Relation-like NAT -defined the carrier of F_Real * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n,n, the carrier of F_Real
Mx2Tran p is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total additive FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
TOP-REAL n is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty set
q is V11() real ext-real set
TR is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q * TR is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q * TR is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(Mx2Tran p) . (q * TR) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
(Mx2Tran p) . TR is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q * ((Mx2Tran p) . TR) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q * ((Mx2Tran p) . TR) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
TOP-REAL n is non empty TopSpace-like right_complementable constituted-Functions constituted-FinSeqs V189() V190() V191() V192() V193() V194() V195() V228() L16()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty Relation-like set
bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is non empty set
q is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total FinSequence-yielding homogeneous Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
p is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total FinSequence-yielding homogeneous Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
p * q is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
f is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q . f is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
dom (p * q) is non empty set
n1 is V11() real ext-real set
n1 * f is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * f is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(p * q) . (n1 * f) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
q . (n1 * f) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
p . (q . (n1 * f)) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
X is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * X is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * X is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
p . (n1 * X) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
p . X is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * (p . X) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * (p . X) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
(p * q) . f is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * ((p * q) . f) is Relation-like NAT -defined Function-like V36() n -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support Element of the carrier of (TOP-REAL n)
n1 * ((p * q) . f) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of REAL
n1 is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
1. F_Real is V11() real ext-real V61( F_Real ) Element of the carrier of F_Real
the OneF of F_Real is V11() real ext-real Element of the carrier of F_Real
- (1. F_Real) is V11() real ext-real Element of the carrier of F_Real
K534((1. F_Real)) is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
p is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
Seg p is V16() V36() p -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
the multF of F_Real is non empty Relation-like [: the carrier of F_Real, the carrier of F_Real:] -defined the carrier of F_Real -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued associative V287( the carrier of F_Real) Element of bool [:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:]
[: the carrier of F_Real, the carrier of F_Real:] is non empty Relation-like complex-yielding ext-real-valued real-valued set
[:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:] is non empty Relation-like complex-yielding ext-real-valued real-valued set
bool [:[: the carrier of F_Real, the carrier of F_Real:], the carrier of F_Real:] is non empty set
n1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
Seg n1 is V16() V36() n1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= n1 ) } is set
[:(Seg n1),(Seg n1):] is Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
f is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
X is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
[f,X] is set
{f,X} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{f} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{f,X},{f}} is non empty V36() V40() set
f is Relation-like NAT -defined the carrier of F_Real * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of n1,n1, the carrier of F_Real
Indices f is set
X is Relation-like NAT -defined the carrier of F_Real * -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V235() tabular Matrix of p,p, the carrier of F_Real
Indices X is set
[:(Seg p),(Seg p):] is Relation-like RAT -valued INT -valued V36() complex-yielding ext-real-valued real-valued natural-valued set
z is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
fp is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
[z,fp] is set
{z,fp} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{z} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{z,fp},{z}} is non empty V36() V40() set
X * (z,fp) is V11() real ext-real Element of the carrier of F_Real
diagonal_of_Matrix X is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
len (diagonal_of_Matrix X) is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
fp is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
fp + n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
(diagonal_of_Matrix X) | (fp + n) is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg (fp + n) is V16() V36() fp + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= fp + n ) } is set
(diagonal_of_Matrix X) | (Seg (fp + n)) is Relation-like NAT -defined Seg (fp + n) -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | (fp + n)) is V11() real ext-real Element of the carrier of F_Real
fp + 1 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
(fp + 1) + n is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() set
(diagonal_of_Matrix X) | ((fp + 1) + n) is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg ((fp + 1) + n) is non empty V16() V36() (fp + 1) + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= (fp + 1) + n ) } is set
(diagonal_of_Matrix X) | (Seg ((fp + 1) + n)) is Relation-like NAT -defined Seg ((fp + 1) + n) -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | ((fp + 1) + n)) is V11() real ext-real Element of the carrier of F_Real
(fp + 1) + n is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
(fp + n) + 1 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
dom (diagonal_of_Matrix X) is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT
(diagonal_of_Matrix X) | ((fp + 1) + n) is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg ((fp + 1) + n) is non empty V16() V36() (fp + 1) + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= (fp + 1) + n ) } is set
(diagonal_of_Matrix X) | (Seg ((fp + 1) + n)) is Relation-like NAT -defined Seg ((fp + 1) + n) -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
(diagonal_of_Matrix X) . ((fp + 1) + n) is V11() real ext-real Element of REAL
<*((diagonal_of_Matrix X) . ((fp + 1) + n))*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
[1,((diagonal_of_Matrix X) . ((fp + 1) + n))] is set
{1,((diagonal_of_Matrix X) . ((fp + 1) + n))} is non empty V36() V155() V156() V157() set
{{1,((diagonal_of_Matrix X) . ((fp + 1) + n))},{1}} is non empty V36() V40() set
{[1,((diagonal_of_Matrix X) . ((fp + 1) + n))]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
((diagonal_of_Matrix X) | (fp + n)) ^ <*((diagonal_of_Matrix X) . ((fp + 1) + n))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like finite-support set
[((fp + 1) + n),((fp + 1) + n)] is set
{((fp + 1) + n),((fp + 1) + n)} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{((fp + 1) + n)} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{((fp + 1) + n),((fp + 1) + n)},{((fp + 1) + n)}} is non empty V36() V40() set
X * (((fp + 1) + n),((fp + 1) + n)) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real "**" ((diagonal_of_Matrix X) | ((fp + 1) + n)) is V11() real ext-real Element of the carrier of F_Real
(- (1. F_Real)) * (1. F_Real) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((- (1. F_Real)),(1. F_Real)) is V11() real ext-real Element of the carrier of F_Real
K538((- (1. F_Real)),(1. F_Real)) is V11() real ext-real Element of REAL
(diagonal_of_Matrix X) | {} is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued the carrier of F_Real -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() FinSequence of the carrier of F_Real
Seg {} is empty ordinal natural V11() real ext-real non positive non negative V16() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element {} -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= {} ) } is set
(diagonal_of_Matrix X) | (Seg {}) is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Seg {} -defined NAT -defined RAT -valued the carrier of F_Real -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() set
the multF of F_Real "**" ((diagonal_of_Matrix X) | {}) is V11() real ext-real Element of the carrier of F_Real
<*> the carrier of F_Real is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined the carrier of F_Real -valued Function-like one-to-one constant functional V36() V37() V40() cardinal {} -element V85() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued V155() V156() V157() V158() V159() V160() V161() FinSequence-yielding finite-support Function-yielding V235() V282() Element of the carrier of F_Real *
the_unity_wrt the multF of F_Real is V11() real ext-real Element of the carrier of F_Real
p - n is V11() real ext-real V85() set
- n is V11() real ext-real non positive V85() set
p + (- n) is V11() real ext-real V85() set
(p - n) + n is V11() real ext-real V85() set
Det X is V11() real ext-real Element of the carrier of F_Real
X * (n,n) is V11() real ext-real Element of the carrier of F_Real
fp is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
(diagonal_of_Matrix X) | fp is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg fp is V16() V36() fp -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= fp ) } is set
(diagonal_of_Matrix X) | (Seg fp) is Relation-like NAT -defined Seg fp -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | fp) is V11() real ext-real Element of the carrier of F_Real
fp + 1 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
(diagonal_of_Matrix X) | (fp + 1) is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg (fp + 1) is non empty V16() V36() fp + 1 -element fp + 1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= fp + 1 ) } is set
(diagonal_of_Matrix X) | (Seg (fp + 1)) is Relation-like NAT -defined Seg (fp + 1) -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | (fp + 1)) is V11() real ext-real Element of the carrier of F_Real
dom (diagonal_of_Matrix X) is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT
(diagonal_of_Matrix X) . (fp + 1) is V11() real ext-real Element of REAL
<*((diagonal_of_Matrix X) . (fp + 1))*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
[1,((diagonal_of_Matrix X) . (fp + 1))] is set
{1,((diagonal_of_Matrix X) . (fp + 1))} is non empty V36() V155() V156() V157() set
{{1,((diagonal_of_Matrix X) . (fp + 1))},{1}} is non empty V36() V40() set
{[1,((diagonal_of_Matrix X) . (fp + 1))]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
((diagonal_of_Matrix X) | fp) ^ <*((diagonal_of_Matrix X) . (fp + 1))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like finite-support set
[(fp + 1),(fp + 1)] is set
{(fp + 1),(fp + 1)} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{(fp + 1)} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{(fp + 1),(fp + 1)},{(fp + 1)}} is non empty V36() V40() set
X * ((fp + 1),(fp + 1)) is V11() real ext-real Element of the carrier of F_Real
(1. F_Real) * (1. F_Real) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((1. F_Real),(1. F_Real)) is V11() real ext-real Element of the carrier of F_Real
K538((1. F_Real),(1. F_Real)) is V11() real ext-real Element of REAL
{} + n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
(diagonal_of_Matrix X) | ({} + n) is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg ({} + n) is V16() V36() {} + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= {} + n ) } is set
(diagonal_of_Matrix X) | (Seg ({} + n)) is Relation-like NAT -defined Seg ({} + n) -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | ({} + n)) is V11() real ext-real Element of the carrier of F_Real
n - 1 is V11() real ext-real V85() Element of REAL
n + (- 1) is V11() real ext-real V85() set
fp is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
fp + 1 is non empty ordinal natural V11() real ext-real positive non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
(diagonal_of_Matrix X) | fp is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg fp is V16() V36() fp -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= fp ) } is set
(diagonal_of_Matrix X) | (Seg fp) is Relation-like NAT -defined Seg fp -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | fp) is V11() real ext-real Element of the carrier of F_Real
dom (diagonal_of_Matrix X) is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT
(diagonal_of_Matrix X) | n is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
Seg n is V16() V36() n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b₁ where b₁ is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
(diagonal_of_Matrix X) | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
(diagonal_of_Matrix X) . n is V11() real ext-real Element of REAL
<*((diagonal_of_Matrix X) . n)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() 1 -element FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued V149() decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
[1,((diagonal_of_Matrix X) . n)] is set
{1,((diagonal_of_Matrix X) . n)} is non empty V36() V155() V156() V157() set
{{1,((diagonal_of_Matrix X) . n)},{1}} is non empty V36() V40() set
{[1,((diagonal_of_Matrix X) . n)]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
((diagonal_of_Matrix X) | fp) ^ <*((diagonal_of_Matrix X) . n)*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like finite-support set
[n,n] is set
{n,n} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{n} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{n,n},{n}} is non empty V36() V40() set
(1. F_Real) * (- (1. F_Real)) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((1. F_Real),(- (1. F_Real))) is V11() real ext-real Element of the carrier of F_Real
K538((1. F_Real),(- (1. F_Real))) is V11() real ext-real Element of REAL
(diagonal_of_Matrix X) | p is Relation-like NAT -defined the carrier of F_Real -valued Function-like V36() FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support FinSequence of the carrier of F_Real
(diagonal_of_Matrix X) | (Seg p) is Relation-like NAT -defined Seg p -defined NAT -defined the carrier of F_Real -valued Function-like V36() FinSubsequence-like complex-yielding ext-real-valued real-valued finite-support set
the multF of F_Real "**" ((diagonal_of_Matrix X) | p) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real "**" (diagonal_of_Matrix X) is V11() real ext-real Element of the carrier of F_Real
[n,n] is set
{n,n} is non empty V36() V40() V155() V156() V157() V158() V159() V160() set
{n} is non empty trivial V36() V40() 1 -element V155() V156() V157() V158() V159() V160() set
{{n,n},{n}} is non empty V36() V40() set
fp is ordinal natural V11() real ext-real non negative V36() cardinal V85() set
X * (fp,fp) is V11() real