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

bool is non empty non trivial V36() set
K375() is non empty strict multMagma
the carrier of K375() is non empty 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

bool [:1,1:] is non empty V36() V40() set

bool [:[:1,1:],1:] is non empty V36() V40() set

bool [:[:1,1:],REAL:] is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool [:[:2,2:],REAL:] is non empty non trivial V36() set

the carrier of () is non empty set

bool is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool is non empty non trivial V36() set

bool is non empty set
K610() is set

K74(0,1,2) is non empty V36() V155() V156() V157() V158() V159() V160() 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

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

bool is non empty non trivial V36() set

bool 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

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

the carrier of () is non empty set

{(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
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= 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

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

Seg n is V16() V36() n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

bool [:(Seg n),(Seg n):] is non empty V36() V40() set

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

Det q is Element of the carrier of p
Indices q is set

Det ((((q * TR) @) * TR) @) is Element of the carrier of p
Permutations n is non empty permutational set
len () is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT
Seg (len ()) is V16() V36() len () -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
- (Det q) is Element of the carrier of p
- (- (Det q)) is Element of the carrier of p

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

TR . f is ordinal natural V11() real ext-real non negative V36() cardinal V85() Element of REAL

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

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

Indices q is 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

dom p is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT

Sum (sqr p) is V11() real ext-real Element 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

q -' 1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT

Seg (q -' 1) is V16() V36() q -' 1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= q -' 1 ) } is set

TR is V11() real ext-real Element 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

TR ^2 is V11() real ext-real Element of REAL
TR * TR is V11() real ext-real set

[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

(((@ (@ 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)) | (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))) ^ (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

[1,z] is set
{1,z} is non empty V36() V155() V156() V157() set
{{1,z},{1}} is non empty V36() V40() set

z ^2 is V11() real ext-real Element of REAL
z * z is V11() real ext-real set

[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

(((@ (@ 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 -' 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 ((@ (@ 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))) ^ ()) is V11() real ext-real Element of REAL
(Sum ((sqr ((@ (@ p)) | (q -' 1))) ^ ())) + (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

dom p is 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

dom q is set

n1 is set
(q . TR) . n1 is set
TR . n1 is set
n is set
p is set
n /\ p is set

dom q is set

n1 is set
(q . TR) . n1 is set
TR . n1 is set
n \/ p is 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) . X is set
q . (TR . f) is Relation-like Function-like set
dom q is set

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] 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

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
the non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total homogeneous Element of bool [: the carrier of (), the carrier of ():] is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total homogeneous Element of bool [: the carrier of (), the carrier of ():]

the carrier of () is non empty set

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
q is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of (), the carrier of ():]
TR is set
dom q is non empty set
rng q is non empty set
q . TR is set

Mx2Tran q is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]
the carrier of () is non empty set
the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set

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

the addF of () is non empty Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty Relation-like set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((() . 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 ()

Mx2Tran p is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total additive FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
q is V11() real ext-real set

the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
q is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total FinSequence-yielding homogeneous Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]
p is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total FinSequence-yielding homogeneous Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]
p * q is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]

dom (p * q) is non empty set
n1 is V11() real ext-real set

n1 is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like total quasi_total FinSequence-yielding Function-yielding V235() Element of bool [: the carrier of (), the carrier of ():]
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
- () is V11() real ext-real Element of the carrier of F_Real
K534(()) is V11() real ext-real Element of REAL

Seg p is V16() V36() p -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= n1 ) } is 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

Indices f is set

Indices X is 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

len is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT

fp + n is ordinal natural V11() real ext-real non negative V36() cardinal V85() set

Seg (fp + n) is V16() V36() fp + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= fp + n ) } is set

the multF of F_Real "**" ( | (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

Seg ((fp + 1) + n) is non empty V16() V36() (fp + 1) + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= (fp + 1) + n ) } is set

the multF of F_Real "**" ( | ((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 is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT

Seg ((fp + 1) + n) is non empty V16() V36() (fp + 1) + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= (fp + 1) + n ) } is set

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

[1,( . ((fp + 1) + n))] is set
{1,( . ((fp + 1) + n))} is non empty V36() V155() V156() V157() set
{{1,( . ((fp + 1) + n))},{1}} is non empty V36() V40() set
{[1,( . ((fp + 1) + n))]} is non empty trivial Relation-like Function-like constant V36() 1 -element finite-support set
( | (fp + n)) ^ <*( . ((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 "**" ( | ((fp + 1) + n)) is V11() real ext-real Element of the carrier of F_Real
(- ()) * () is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((- ()),()) is V11() real ext-real Element of the carrier of F_Real
K538((- ()),()) is V11() real ext-real Element of REAL

{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= {} ) } is set

the multF of F_Real "**" () is V11() real ext-real 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

Seg fp is V16() V36() fp -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= fp ) } is set

the multF of F_Real "**" ( | 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

Seg (fp + 1) is non empty V16() V36() fp + 1 -element fp + 1 -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= fp + 1 ) } is set

the multF of F_Real "**" ( | (fp + 1)) is V11() real ext-real Element of the carrier of F_Real
dom is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT
. (fp + 1) is V11() real ext-real Element of REAL

[1,( . (fp + 1))] is set
{1,( . (fp + 1))} is non empty V36() V155() V156() V157() set
{{1,( . (fp + 1))},{1}} is non empty V36() V40() set
{[1,( . (fp + 1))]} is non empty trivial Relation-like Function-like constant V36() 1 -element 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
() * () is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((),()) is V11() real ext-real Element of the carrier of F_Real
K538((),()) is V11() real ext-real Element of REAL

Seg ({} + n) is V16() V36() {} + n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= {} + n ) } is set

the multF of F_Real "**" ( | ({} + 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 + 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

Seg fp is V16() V36() fp -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= fp ) } is set

the multF of F_Real "**" ( | fp) is V11() real ext-real Element of the carrier of F_Real
dom is V36() V155() V156() V157() V158() V159() V160() Element of bool NAT

Seg n is V16() V36() n -element V155() V156() V157() V158() V159() V160() Element of bool NAT
{ b1 where b1 is ordinal natural V11() real ext-real non negative V36() cardinal V85() V86() V155() V156() V157() V158() V159() V160() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

[1,( . n)] is set
{1,( . n)} is non empty V36() V155() V156() V157() set
{{1,( . n)},{1}} is non empty V36() V40() 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
() * (- ()) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real . ((),(- ())) is V11() real ext-real Element of the carrier of F_Real
K538((),(- ())) is V11() real ext-real Element of REAL

the multF of F_Real "**" ( | p) is V11() real ext-real Element of the carrier of F_Real
the multF of F_Real "**" 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

X * (fp,fp) is V11() real