REAL is non empty V47() V167() V168() V169() V173() V220() V221() V223() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V52() V53() V167() V168() V169() V170() V171() V172() V173() V218() V220() Element of bool REAL
bool REAL is V47() set
INT is non empty V47() V167() V168() V169() V170() V171() V173() set
COMPLEX is non empty V47() V167() V173() set
RAT is non empty V47() V167() V168() V169() V170() V173() set
[:COMPLEX,COMPLEX:] is V47() complex-yielding set
bool [:COMPLEX,COMPLEX:] is V47() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V47() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V47() set
[:REAL,REAL:] is V47() complex-yielding V158() V159() set
bool [:REAL,REAL:] is V47() set
[:[:REAL,REAL:],REAL:] is V47() complex-yielding V158() V159() set
bool [:[:REAL,REAL:],REAL:] is V47() set
[:RAT,RAT:] is RAT -valued V47() complex-yielding V158() V159() set
bool [:RAT,RAT:] is V47() set
[:[:RAT,RAT:],RAT:] is RAT -valued V47() complex-yielding V158() V159() set
bool [:[:RAT,RAT:],RAT:] is V47() set
[:INT,INT:] is RAT -valued INT -valued V47() complex-yielding V158() V159() set
bool [:INT,INT:] is V47() set
[:[:INT,INT:],INT:] is RAT -valued INT -valued V47() complex-yielding V158() V159() set
bool [:[:INT,INT:],INT:] is V47() set
[:NAT,NAT:] is RAT -valued INT -valued V47() complex-yielding V158() V159() V160() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V47() complex-yielding V158() V159() V160() set
bool [:[:NAT,NAT:],NAT:] is V47() set
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V52() V53() V167() V168() V169() V170() V171() V172() V173() V218() V220() set
bool omega is V47() set
bool NAT is V47() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
K333() is V109() L11()
the U1 of K333() is set
the U1 of K333() * is non empty functional FinSequence-membered FinSequenceSet of the U1 of K333()
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V47() V52() V54( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() V220() V221() V222() V223() set
{{},1} is non empty V167() V168() V169() V170() V171() V172() V218() V220() set
[:NAT,REAL:] is V47() complex-yielding V158() V159() set
bool [:NAT,REAL:] is V47() set
[:NAT,COMPLEX:] is V47() complex-yielding set
bool [:NAT,COMPLEX:] is V47() set
PFuncs (REAL,REAL) is set
[:NAT,(PFuncs (REAL,REAL)):] is set
bool [:NAT,(PFuncs (REAL,REAL)):] is set
ExtREAL is non empty V168() V223() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() functional V32() V47() V52() V54( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() V220() V221() V222() V223() Element of NAT
Seg 1 is non empty trivial V47() V54(1) V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of bool NAT
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like NAT -defined REAL -valued Function-like functional V47() V52() V54( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V158() V159() V160() V167() V168() V169() V170() V171() V172() V173() V220() V221() V222() V223() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
number_e is V11() real ext-real Element of REAL
right_open_halfline 0 is V167() V168() V169() V210() Element of bool REAL
+infty is non empty non real ext-real positive non negative set
K600(0,+infty) is V218() V219() V223() set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= 0 & not +infty <= b1 ) } is set
ln is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
log_ number_e is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
K582() is Relation-like REAL -defined REAL -valued Function-like V29( REAL , REAL ) complex-yielding V158() V159() Element of bool [:REAL,REAL:]
K540(REAL,REAL,K582()) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
K647(REAL,ln) is V167() V168() V169() Element of bool REAL
K648(REAL,ln) is V167() V168() V169() Element of bool REAL
dom {} is set
rng {} is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M div p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 div p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 mod p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M mod p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M + (M mod p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M - (M mod p) is V11() real ext-real Element of REAL
K38((M mod p)) is V11() real ext-real non positive set
K36(M,K38((M mod p))) is V11() real ext-real set
(M + (M mod p)) - (M mod p) is V11() real ext-real Element of REAL
K36((M + (M mod p)),K38((M mod p))) is V11() real ext-real set
M1 / p is V11() real ext-real non negative Element of REAL
K39(p) is V11() real ext-real non negative set
K37(M1,K39(p)) is V11() real ext-real non negative set
(M - (M mod p)) / p is V11() real ext-real Element of REAL
K37((M - (M mod p)),K39(p)) is V11() real ext-real set
p * (M div p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(p * (M div p)) + (M mod p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p / p is V11() real ext-real non negative Element of REAL
K37(p,K39(p)) is V11() real ext-real non negative set
(p / p) * (M div p) is V11() real ext-real non negative Element of REAL
1 * (M div p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 div p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p * (M1 div p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(p * (M1 div p)) + (M1 mod p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(p / p) * (M1 div p) is V11() real ext-real non negative Element of REAL
1 * (M1 div p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p is V11() real ext-real Element of REAL
ln . p is V11() real ext-real Element of REAL
p - 1 is V11() real ext-real Element of REAL
K38(1) is V11() real ext-real non positive set
K36(p,K38(1)) is V11() real ext-real set
].0,1.[ is V167() V168() V169() V210() V218() V219() V223() Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= 0 & not 1 <= b1 ) } is set
right_open_halfline 1 is V167() V168() V169() V210() Element of bool REAL
K600(1,+infty) is V218() V219() V223() set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= 1 & not +infty <= b1 ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= 0 } is set
L is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
dom L is set
- 1 is V11() real ext-real non positive Element of REAL
M3 is V11() real ext-real Element of REAL
L . M3 is V11() real ext-real Element of REAL
1 * M3 is V11() real ext-real Element of REAL
(1 * M3) + (- 1) is V11() real ext-real Element of REAL
M3 - 1 is V11() real ext-real Element of REAL
K36(M3,K38(1)) is V11() real ext-real set
M1 is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
L - M1 is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
- M1 is Relation-like Function-like complex-yielding set
K38(1) * M1 is Relation-like Function-like set
L + (- M1) is Relation-like Function-like set
dom M1 is set
dom (L - M1) is set
(right_open_halfline 0) /\ REAL is V167() V168() V169() set
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
L2 - 1 is V11() real ext-real Element of REAL
K36(L2,K38(1)) is V11() real ext-real set
ln . L2 is V11() real ext-real Element of REAL
(L2 - 1) - (ln . L2) is V11() real ext-real Element of REAL
K38((ln . L2)) is V11() real ext-real set
K36((L2 - 1),K38((ln . L2))) is V11() real ext-real set
L . L2 is V11() real ext-real Element of REAL
M1 . L2 is V11() real ext-real Element of REAL
(L . L2) - (M1 . L2) is V11() real ext-real Element of REAL
K38((M1 . L2)) is V11() real ext-real set
K36((L . L2),K38((M1 . L2))) is V11() real ext-real set
(L - M1) . 1 is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real Element of REAL
K36(1,K38(1)) is V11() real ext-real set
ln . 1 is V11() real ext-real Element of REAL
(1 - 1) - (ln . 1) is V11() real ext-real Element of REAL
K38((ln . 1)) is V11() real ext-real set
K36((1 - 1),K38((ln . 1))) is V11() real ext-real set
log (number_e,1) is V11() real ext-real Element of REAL
- (log (number_e,1)) is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V47() V52() V54( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() V220() V221() V222() V223() Element of REAL
L2 is V11() real ext-real Element of REAL
diff (L,L2) is V11() real ext-real Element of REAL
L `| (right_open_halfline 0) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
(L `| (right_open_halfline 0)) . L2 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) `| (right_open_halfline 0) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
((L - M1) `| (right_open_halfline 0)) . L2 is V11() real ext-real Element of REAL
diff (L,L2) is V11() real ext-real Element of REAL
diff (M1,L2) is V11() real ext-real Element of REAL
(diff (L,L2)) - (diff (M1,L2)) is V11() real ext-real Element of REAL
K38((diff (M1,L2))) is V11() real ext-real set
K36((diff (L,L2)),K38((diff (M1,L2)))) is V11() real ext-real set
1 - (diff (M1,L2)) is V11() real ext-real Element of REAL
K36(1,K38((diff (M1,L2)))) is V11() real ext-real set
1 / L2 is V11() real ext-real Element of REAL
K39(L2) is V11() real ext-real set
K37(1,K39(L2)) is V11() real ext-real set
1 - (1 / L2) is V11() real ext-real Element of REAL
K38((1 / L2)) is V11() real ext-real set
K36(1,K38((1 / L2))) is V11() real ext-real set
diff ((L - M1),L2) is V11() real ext-real Element of REAL
(L - M1) | (right_open_halfline 0) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
L2 is V11() real ext-real Element of REAL
diff ((L - M1),L2) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= 1 } is set
1 / L2 is V11() real ext-real Element of REAL
K39(L2) is V11() real ext-real set
K37(1,K39(L2)) is V11() real ext-real set
1 - (1 / L2) is V11() real ext-real Element of REAL
K38((1 / L2)) is V11() real ext-real set
K36(1,K38((1 / L2))) is V11() real ext-real set
p2 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
[.1,L2.] is V167() V168() V169() V209() V223() Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( 1 <= b1 & b1 <= L2 ) } is set
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= 1 } is set
].1,L2.[ is V167() V168() V169() V210() V218() V219() V223() Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= 1 & not L2 <= b1 ) } is set
(L - M1) | [.1,L2.] is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
diff ((L - M1),p2) is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
((L - M1) . L2) - ((L - M1) . 1) is V11() real ext-real Element of REAL
K38(((L - M1) . 1)) is V11() real ext-real set
K36(((L - M1) . L2),K38(((L - M1) . 1))) is V11() real ext-real set
L2 - 1 is V11() real ext-real Element of REAL
K36(L2,K38(1)) is V11() real ext-real set
(((L - M1) . L2) - ((L - M1) . 1)) / (L2 - 1) is V11() real ext-real Element of REAL
K39((L2 - 1)) is V11() real ext-real set
K37((((L - M1) . L2) - ((L - M1) . 1)),K39((L2 - 1))) is V11() real ext-real set
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
diff ((L - M1),p2) is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= 1 } is set
L2 is V11() real ext-real Element of REAL
diff ((L - M1),L2) is V11() real ext-real Element of REAL
1 / L2 is V11() real ext-real Element of REAL
K39(L2) is V11() real ext-real set
K37(1,K39(L2)) is V11() real ext-real set
p2 is V11() real ext-real Element of REAL
1 - (1 / L2) is V11() real ext-real Element of REAL
K38((1 / L2)) is V11() real ext-real set
K36(1,K38((1 / L2))) is V11() real ext-real set
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
[.L2,1.] is V167() V168() V169() V209() V223() Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( L2 <= b1 & b1 <= 1 ) } is set
(L - M1) | [.L2,1.] is Relation-like REAL -defined REAL -valued Function-like complex-yielding V158() V159() Element of bool [:REAL,REAL:]
p2 is V11() real ext-real Element of REAL
].L2,1.[ is V167() V168() V169() V210() V218() V219() V223() Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= L2 & not 1 <= b1 ) } is set
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
diff ((L - M1),p2) is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
1 - L2 is V11() real ext-real Element of REAL
K38(L2) is V11() real ext-real set
K36(1,K38(L2)) is V11() real ext-real set
p2 is V11() real ext-real Element of REAL
((L - M1) . 1) - ((L - M1) . L2) is V11() real ext-real Element of REAL
K38(((L - M1) . L2)) is V11() real ext-real set
K36(((L - M1) . 1),K38(((L - M1) . L2))) is V11() real ext-real set
(((L - M1) . 1) - ((L - M1) . L2)) / (1 - L2) is V11() real ext-real Element of REAL
K39((1 - L2)) is V11() real ext-real set
K37((((L - M1) . 1) - ((L - M1) . L2)),K39((1 - L2))) is V11() real ext-real set
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real Element of REAL
diff ((L - M1),p2) is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
L2 is V11() real ext-real Element of REAL
(L - M1) . L2 is V11() real ext-real Element of REAL
(L - M1) . p is V11() real ext-real Element of REAL
(p - 1) - (ln . p) is V11() real ext-real Element of REAL
K38((ln . p)) is V11() real ext-real set
K36((p - 1),K38((ln . p))) is V11() real ext-real set
(p - 1) - 0 is V11() real ext-real Element of REAL
K38(0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V47() V52() V54( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() V220() V221() V222() V223() set
K36((p - 1),K38(0)) is V11() real ext-real set
1 - p is V11() real ext-real Element of REAL
K38(p) is V11() real ext-real set
K36(1,K38(p)) is V11() real ext-real set
p is V11() real ext-real Element of REAL
log (number_e,p) is V11() real ext-real Element of REAL
p - 1 is V11() real ext-real Element of REAL
K38(1) is V11() real ext-real non positive set
K36(p,K38(1)) is V11() real ext-real set
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= 0 } is set
ln . p is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
log (p,M) is V11() real ext-real Element of REAL
p to_power (log (p,M)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
log (p,M) is V11() real ext-real Element of REAL
- (log (p,M)) is V11() real ext-real Element of REAL
1 / M is V11() real ext-real Element of REAL
K39(M) is V11() real ext-real set
K37(1,K39(M)) is V11() real ext-real set
log (p,(1 / M)) is V11() real ext-real Element of REAL
0 - (log (p,M)) is V11() real ext-real Element of REAL
K38((log (p,M))) is V11() real ext-real set
K36(0,K38((log (p,M)))) is V11() real ext-real set
log (p,1) is V11() real ext-real Element of REAL
(log (p,1)) - (log (p,M)) is V11() real ext-real Element of REAL
K36((log (p,1)),K38((log (p,M)))) is V11() real ext-real set
p is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
log (p,M) is V11() real ext-real Element of REAL
M1 is V11() real ext-real Element of REAL
M * M1 is V11() real ext-real Element of REAL
log (p,(M * M1)) is V11() real ext-real Element of REAL
(M * M1) * (log (p,(M * M1))) is V11() real ext-real Element of REAL
(M * M1) * (log (p,M)) is V11() real ext-real Element of REAL
log (p,M1) is V11() real ext-real Element of REAL
(M * M1) * (log (p,M1)) is V11() real ext-real Element of REAL
((M * M1) * (log (p,M))) + ((M * M1) * (log (p,M1))) is V11() real ext-real Element of REAL
(log (p,M)) + (log (p,M1)) is V11() real ext-real Element of REAL
(M * M1) * ((log (p,M)) + (log (p,M1))) is V11() real ext-real Element of REAL
M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Sum p is V11() real ext-real Element of REAL
Sum M is V11() real ext-real Element of REAL
Sum M1 is V11() real ext-real Element of REAL
(Sum M) + (Sum M1) is V11() real ext-real Element of REAL
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M1 is V11() real ext-real Element of REAL
M /. M1 is V11() real ext-real Element of REAL
M1 /. M1 is V11() real ext-real Element of REAL
(M /. M1) + (M1 /. M1) is V11() real ext-real Element of REAL
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M . M1 is V11() real ext-real Element of REAL
M1 . M1 is V11() real ext-real Element of REAL
(M . M1) + (M1 . M1) is V11() real ext-real Element of REAL
(M /. M1) + (M1 . M1) is V11() real ext-real Element of REAL
M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Sum p is V11() real ext-real Element of REAL
Sum M is V11() real ext-real Element of REAL
Sum M1 is V11() real ext-real Element of REAL
(Sum M) - (Sum M1) is V11() real ext-real Element of REAL
K38((Sum M1)) is V11() real ext-real set
K36((Sum M),K38((Sum M1))) is V11() real ext-real set
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M1 is V11() real ext-real Element of REAL
M /. M1 is V11() real ext-real Element of REAL
M1 /. M1 is V11() real ext-real Element of REAL
(M /. M1) - (M1 /. M1) is V11() real ext-real Element of REAL
K38((M1 /. M1)) is V11() real ext-real set
K36((M /. M1),K38((M1 /. M1))) is V11() real ext-real set
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M . M1 is V11() real ext-real Element of REAL
M1 . M1 is V11() real ext-real Element of REAL
(M . M1) - (M1 . M1) is V11() real ext-real Element of REAL
K38((M1 . M1)) is V11() real ext-real set
K36((M . M1),K38((M1 . M1))) is V11() real ext-real set
(M /. M1) - (M1 . M1) is V11() real ext-real Element of REAL
K36((M /. M1),K38((M1 . M1))) is V11() real ext-real set
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . 1 is V11() real ext-real Element of REAL
Sum p is V11() real ext-real Element of REAL
M is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
M . 1 is V11() real ext-real Element of REAL
M . (len p) is V11() real ext-real Element of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M1 is Relation-like NAT -defined Function-like V47() FinSequence-like FinSubsequence-like set
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
rng M1 is set
M1 is set
M2 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M1 . M2 is set
M . M2 is V11() real ext-real Element of REAL
M2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
M1 . (M2 + 1) is V11() real ext-real Element of REAL
M . (M2 + 1) is V11() real ext-real Element of REAL
M . M2 is V11() real ext-real Element of REAL
p . (M2 + 1) is V11() real ext-real Element of REAL
(M . M2) + (p . (M2 + 1)) is V11() real ext-real Element of REAL
M1 . M2 is V11() real ext-real Element of REAL
(M1 . M2) + (p . (M2 + 1)) is V11() real ext-real Element of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 . 1 is V11() real ext-real Element of REAL
M1 . (len p) is V11() real ext-real Element of REAL
M2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
M1 . (M2 + 1) is V11() real ext-real Element of REAL
M1 . M2 is V11() real ext-real Element of REAL
p . (M2 + 1) is V11() real ext-real Element of REAL
(M1 . M2) + (p . (M2 + 1)) is V11() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M is V11() real ext-real Element of REAL
rng p is V167() V168() V169() Element of bool REAL
M is V11() real ext-real set
rng p is V167() V168() V169() set
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
p . M1 is V11() real ext-real Element of REAL
<*1*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one V47() V54(1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V161() V162() V163() V164() FinSequence of REAL
dom <*1*> is non empty trivial V54(1) V167() V168() V169() V170() V171() V172() V218() V220() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
<*1*> . M is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
p * M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
dom (p * M) is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M . M1 is V11() real ext-real Element of REAL
(p * M) . M1 is V11() real ext-real Element of REAL
p * (M . M1) is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
M1 . M is V11() real ext-real Element of REAL
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M . p is V11() real ext-real Element of REAL
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
mlt (M,M1) is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
(mlt (M,M1)) . p is V11() real ext-real Element of REAL
M1 . p is V11() real ext-real Element of REAL
(M . p) * (M1 . p) is V11() real ext-real Element of REAL
len (mlt (M,M1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
dom (mlt (M,M1)) is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(mlt (M,M1)) . M1 is V11() real ext-real Element of REAL
M . M1 is V11() real ext-real Element of REAL
M1 . M1 is V11() real ext-real Element of REAL
(M . M1) * (M1 . M1) is V11() real ext-real Element of REAL
0 * (M1 . M1) is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
Sum M is V11() real ext-real Element of REAL
M . p is V11() real ext-real Element of REAL
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Seg p is V47() V54(p) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
M | (Seg p) is Relation-like NAT -defined REAL -valued Function-like FinSubsequence-like complex-yielding V158() V159() Element of bool [:NAT,REAL:]
M1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
M2 is Relation-like NAT -defined Function-like V47() FinSequence-like FinSubsequence-like set
M1 ^ M2 is Relation-like NAT -defined Function-like V47() FinSequence-like FinSubsequence-like set
L is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom L is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
len L is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Seg (len L) is V47() V54( len L) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
(dom M) /\ (Seg p) is V167() V168() V169() V170() V171() V172() V220() set
dom M1 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
L . M3 is V11() real ext-real Element of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(len M1) + M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M . ((len M1) + M3) is V11() real ext-real Element of REAL
M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
L . M3 is V11() real ext-real Element of REAL
(len L) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V47() V54( len L) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V160() Element of (len L) -tuples_on NAT
(len L) -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V47() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = len L } is set
(Seg (len L)) --> 0 is Relation-like Seg (len L) -defined INT -valued RAT -valued {0} -valued Function-like V29( Seg (len L),{0}) V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() V160() Element of bool [:(Seg (len L)),{0}:]
{0} is non empty trivial V54(1) V167() V168() V169() V170() V171() V172() V218() V220() set
[:(Seg (len L)),{0}:] is INT -valued RAT -valued complex-yielding V158() V159() V160() set
bool [:(Seg (len L)),{0}:] is set
((len L) |-> 0) . M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative Element of REAL
len M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M3 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
L2 is V11() real ext-real Element of REAL
<*L2*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one V47() V54(1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V161() V162() V163() V164() FinSequence of REAL
M3 ^ <*L2*> is non empty Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
len M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
len <*L2*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
(len M3) + (len <*L2*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
(len M3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
M1 . p is V11() real ext-real Element of REAL
M1 is V11() real ext-real Element of REAL
dom M3 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Seg (len M3) is V47() V54( len M3) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
p2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M3 . p2 is V11() real ext-real Element of REAL
M1 . p2 is V11() real ext-real Element of REAL
M . p2 is V11() real ext-real Element of REAL
p2 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M3 . p2 is V11() real ext-real Element of REAL
(len M3) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V47() V54( len M3) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V160() Element of (len M3) -tuples_on NAT
(len M3) -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V47() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = len M3 } is set
(Seg (len M3)) --> 0 is Relation-like Seg (len M3) -defined INT -valued RAT -valued {0} -valued Function-like V29( Seg (len M3),{0}) V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() V160() Element of bool [:(Seg (len M3)),{0}:]
[:(Seg (len M3)),{0}:] is INT -valued RAT -valued complex-yielding V158() V159() V160() set
bool [:(Seg (len M3)),{0}:] is set
((len M3) |-> 0) . p2 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative Element of REAL
len ((len M3) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
len ((len L) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Sum (M3 ^ <*L2*>) is V11() real ext-real Element of REAL
Sum ((len L) |-> 0) is V11() real ext-real set
(Sum (M3 ^ <*L2*>)) + (Sum ((len L) |-> 0)) is V11() real ext-real Element of REAL
(Sum (M3 ^ <*L2*>)) + 0 is V11() real ext-real Element of REAL
Sum ((len M3) |-> 0) is V11() real ext-real set
(Sum ((len M3) |-> 0)) + L2 is V11() real ext-real Element of REAL
0 + M1 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Sum p is V11() real ext-real Element of REAL
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M is V11() real ext-real Element of REAL
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M + M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M2 is V11() real ext-real Element of REAL
M2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M2 is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M2 + L is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M3 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
L2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len L2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len p2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
L2 ^ p2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p2 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
p2 . p1 is V11() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
M2 + p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . (M2 + p1) is V11() real ext-real Element of REAL
Seg M2 is V47() V54(M2) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
dom L2 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
L2 . M2 is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
L2 . p1 is V11() real ext-real Element of REAL
p . p1 is V11() real ext-real Element of REAL
Sum L2 is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M2 + p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p2 . p1 is V11() real ext-real Element of REAL
Sum p2 is V11() real ext-real Element of REAL
(Sum L2) + (Sum p2) is V11() real ext-real Element of REAL
(p . M) + 0 is V11() real ext-real Element of REAL
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
L2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len L2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len p2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
L2 ^ p2 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p2 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
p2 . p1 is V11() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
M + p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . (M + p1) is V11() real ext-real Element of REAL
Seg M is V47() V54(M) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
dom L2 is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
L2 . M is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
L2 . p1 is V11() real ext-real Element of REAL
p . p1 is V11() real ext-real Element of REAL
Sum L2 is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real non negative set
M + p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p2 . p1 is V11() real ext-real Element of REAL
Sum p2 is V11() real ext-real Element of REAL
(Sum L2) + (Sum p2) is V11() real ext-real Element of REAL
(p . M) + 0 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M is V11() real ext-real Element of REAL
p is non empty Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() ProbFinS nonnegative-yielding FinSequence of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p . M is V11() real ext-real Element of REAL
Sum p is V11() real ext-real Element of REAL
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V47() V52() ext-real positive non negative set
1 / p is V11() real ext-real non negative Element of REAL
K39(p) is non empty V11() real ext-real positive non negative set
K37(1,K39(p)) is V11() real ext-real non negative set
p |-> (1 / p) is Relation-like NAT -defined REAL -valued Function-like V47() V54(p) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of p -tuples_on REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = p } is set
Seg p is non empty V47() V54(p) V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of bool NAT
(Seg p) --> (1 / p) is Relation-like Seg p -defined {(1 / p)} -valued Function-like V29( Seg p,{(1 / p)}) V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of bool [:(Seg p),{(1 / p)}:]
{(1 / p)} is non empty trivial V54(1) V167() V168() V169() set
[:(Seg p),{(1 / p)}:] is complex-yielding V158() V159() set
bool [:(Seg p),{(1 / p)}:] is set
M is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real positive non negative V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of NAT
1 / M is V11() real ext-real non negative Element of REAL
K39(M) is non empty V11() real ext-real positive non negative set
K37(1,K39(M)) is V11() real ext-real non negative set
M |-> (1 / M) is Relation-like NAT -defined REAL -valued Function-like V47() V54(M) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of M -tuples_on REAL
M -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = M } is set
Seg M is non empty V47() V54(M) V167() V168() V169() V170() V171() V172() V218() V219() V220() V221() V222() Element of bool NAT
(Seg M) --> (1 / M) is Relation-like Seg M -defined {(1 / M)} -valued Function-like V29( Seg M,{(1 / M)}) V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of bool [:(Seg M),{(1 / M)}:]
{(1 / M)} is non empty trivial V54(1) V167() V168() V169() set
[:(Seg M),{(1 / M)}:] is complex-yielding V158() V159() set
bool [:(Seg M),{(1 / M)}:] is set
dom (M |-> (1 / M)) is V54(M) V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(M |-> (1 / M)) . M1 is V11() real ext-real Element of REAL
Sum (M |-> (1 / M)) is V11() real ext-real Element of REAL
M * (1 / M) is V11() real ext-real non negative Element of REAL
p is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
SumAll p is V11() real ext-real Element of REAL
width p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular Matrix of len p, 0 , REAL
SumAll M is V11() real ext-real Element of REAL
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
width p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
p is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
SumAll p is V11() real ext-real Element of REAL
width p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular Matrix of 0 , width p, REAL
len M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
p is non empty set
p * is non empty functional FinSequence-membered FinSequenceSet of p
M is Relation-like NAT -defined p * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of p *
dom M is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
width M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Seg (width M) is V47() V54( width M) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M . M1 is Relation-like NAT -defined p -valued Function-like V47() FinSequence-like FinSubsequence-like FinSequence of p
dom (M . M1) is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Line (M,M1) is Relation-like NAT -defined p -valued Function-like V47() V54( width M) FinSequence-like FinSubsequence-like Element of (width M) -tuples_on p
(width M) -tuples_on p is non empty functional FinSequence-membered FinSequenceSet of p
{ b1 where b1 is Relation-like NAT -defined p -valued Function-like V47() FinSequence-like FinSubsequence-like Element of p * : len b1 = width M } is set
dom (Line (M,M1)) is V54( width M) V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
len (Line (M,M1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Seg (len (Line (M,M1))) is V47() V54( len (Line (M,M1))) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
p is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Line (p,M) is Relation-like NAT -defined REAL -valued Function-like V47() V54( width p) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width p) -tuples_on REAL
width p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(width p) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = width p } is set
dom (Line (p,M)) is V54( width p) V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
p . M is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom (p . M) is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
Seg (width p) is V47() V54( width p) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
(Line (p,M)) . M1 is V11() real ext-real Element of REAL
p * (M,M1) is V11() real ext-real Element of REAL
[M,M1] is set
{M,M1} is non empty V167() V168() V169() V170() V171() V172() V218() V220() set
{M} is non empty trivial V54(1) V167() V168() V169() V170() V171() V172() V218() V220() set
{{M,M1},{M}} is non empty set
Indices p is set
M is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
[M,M1] is set
{M,M1} is non empty V167() V168() V169() V170() V171() V172() V218() V220() set
{M} is non empty trivial V54(1) V167() V168() V169() V170() V171() V172() V218() V220() set
{{M,M1},{M}} is non empty set
Line (p,M) is Relation-like NAT -defined REAL -valued Function-like V47() V54( width p) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width p) -tuples_on REAL
len (Line (p,M)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Seg (len (Line (p,M))) is V47() V54( len (Line (p,M))) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
dom (Line (p,M)) is V54( width p) V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Seg (len p) is V47() V54( len p) V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of bool NAT
p * (M,M1) is V11() real ext-real Element of REAL
(Line (p,M)) . M1 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom p is V167() V168() V169() V170() V171() V172() V220() Element of bool NAT
LineVec2Mx p is Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
M1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
Col ((LineVec2Mx p),M1) is Relation-like NAT -defined REAL -valued Function-like V47() V54( len (LineVec2Mx p)) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (len (LineVec2Mx p)) -tuples_on REAL
len (LineVec2Mx p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V32() V47() V52() ext-real non negative V167() V168() V169() V170() V171() V172() V220() V221() V222() Element of NAT
(len (LineVec2Mx p)) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len (LineVec2Mx p) } is set
p . M1 is V11() real ext-real Element of REAL
<*(p . M1)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one V47()