:: TOPREAL7 semantic presentation

REAL is non empty V33() V166() V167() V168() V172() set
NAT is V166() V167() V168() V169() V170() V171() V172() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V33() V166() V172() set
NAT is V166() V167() V168() V169() V170() V171() V172() set
bool NAT is non empty set
I[01] is TopStruct
the carrier of I[01] is set
bool NAT is non empty set
1 is non empty V10() V11() V12() ext-real positive V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
RAT is non empty V33() V166() V167() V168() V169() V172() set
[:1,1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
INT is non empty V33() V166() V167() V168() V169() V170() V172() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V16() complex-yielding V141() V142() set
[:[:REAL,REAL:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V10() V11() V12() ext-real positive V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
[:2,2:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
[:[:2,2:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V105() V130() V131() V132() V133() V134() V135() V136() V181() L15()
the carrier of (TOP-REAL 2) is non empty set
the carrier of (TOP-REAL 2) * is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
[:COMPLEX,COMPLEX:] is non empty V16() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V16() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty V16() V20( RAT ) complex-yielding V141() V142() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V16() V20( RAT ) complex-yielding V141() V142() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
[:[:NAT,NAT:],NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is set
the empty V16() non-empty empty-yielding V20( RAT ) complex-yielding V141() V142() V143() V166() V167() V168() V169() V170() V171() V172() set is empty V16() non-empty empty-yielding V20( RAT ) complex-yielding V141() V142() V143() V166() V167() V168() V169() V170() V171() V172() set
0 is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
absreal is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-yielding V141() V142() Element of bool [:REAL,REAL:]
i is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
i + f is V11() V12() ext-real Element of REAL
j is V11() V12() ext-real Element of REAL
c₄ is V11() V12() ext-real Element of REAL
j + c₄ is V11() V12() ext-real Element of REAL
max ((i + f),(j + c₄)) is V11() V12() ext-real Element of REAL
max (i,j) is V11() V12() ext-real Element of REAL
max (f,c₄) is V11() V12() ext-real Element of REAL
(max (i,j)) + (max (f,c₄)) is V11() V12() ext-real Element of REAL
i is V11() V12() ext-real Element of REAL
j is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
j + f is V11() V12() ext-real Element of REAL
c₄ is V11() V12() ext-real Element of REAL
cij is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
cij + f is V11() V12() ext-real Element of REAL
max (i,c₄) is V11() V12() ext-real Element of REAL
max (j,cij) is V11() V12() ext-real Element of REAL
max (f,f) is V11() V12() ext-real Element of REAL
(max (j,cij)) + (max (f,f)) is V11() V12() ext-real Element of REAL
max ((j + f),(cij + f)) is V11() V12() ext-real Element of REAL
j is V16() Function-like FinSequence-like set
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() Function-like FinSequence-like set
i ^ j is V16() Function-like FinSequence-like set
dom (i ^ j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Seg (len j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
Seg ((len i) + (len j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V10() V11() V12() ext-real V89() set
j is V16() Function-like FinSequence-like set
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
f is V16() Function-like FinSequence-like set
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - (len j) is V11() V12() ext-real V89() Element of REAL
dom f is V166() V167() V168() V169() V170() V171() Element of bool NAT
((len j) + (len f)) - (len j) is V11() V12() ext-real V89() Element of REAL
(len j) - (len j) is V11() V12() ext-real V89() Element of REAL
i is V16() Function-like FinSequence-like set
j is V16() Function-like FinSequence-like set
i ^ j is V16() Function-like FinSequence-like set
f is V16() Function-like FinSequence-like set
c₄ is V16() Function-like FinSequence-like set
f ^ c₄ is V16() Function-like FinSequence-like set
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
i . cij is set
f . cij is set
dom f is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
(i ^ j) . cij is set
cij is V10() V11() V12() ext-real V89() set
j . cij is set
c₄ . cij is set
dom c₄ is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) + cij is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(i ^ j) . ((len i) + cij) is set
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
sqr i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (sqr i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
sqr j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
dom (sqr j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
abs i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * i is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
len (abs i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs i) is V166() V167() V168() V169() V170() V171() Element of bool NAT
rng i is V166() V167() V168() Element of bool REAL
dom absreal is V166() V167() V168() Element of bool REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i ^ j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i ^ j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr i) ^ (sqr j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * i is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i ^ j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i ^ j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i ^ j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
abs j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * j is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs i) ^ (abs j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i ^ j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i ^ j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
f is V10() V11() V12() ext-real V89() set
(abs (i ^ j)) . f is V11() V12() ext-real Element of REAL
((abs i) ^ (abs j)) . f is V11() V12() ext-real Element of REAL
dom (i ^ j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs i) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(i ^ j) . f is V11() V12() ext-real Element of REAL
absreal . ((i ^ j) . f) is V11() V12() ext-real Element of REAL
i . f is V11() V12() ext-real Element of REAL
absreal . (i . f) is V11() V12() ext-real Element of REAL
c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i . c₄ is V11() V12() ext-real Element of REAL
abs (i . c₄) is V11() V12() ext-real Element of REAL
(abs i) . c₄ is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
c₄ - (len i) is V11() V12() ext-real V89() Element of REAL
cij is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
len ((abs i) ^ (abs j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(i ^ j) . f is V11() V12() ext-real Element of REAL
absreal . ((i ^ j) . f) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
absreal . (j . cij) is V11() V12() ext-real Element of REAL
abs (j . cij) is V11() V12() ext-real Element of REAL
(abs j) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
len ((abs i) ^ (abs j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i + j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) + (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (f + c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr (i + j)) ^ (sqr (f + c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr ((i ^ f) + (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) + (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f + c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (i + j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i + j))) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i + j))) + (len (sqr (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((sqr (i + j)) ^ (sqr (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(sqr ((i ^ f) + (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((sqr (i + j)) ^ (sqr (f + c₄))) . cij is V11() V12() ext-real Element of REAL
dom (sqr ((i ^ f) + (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) + (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (sqr (i + j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
((i ^ f) + (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) + (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((i . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) + (j . cij) is V11() V12() ext-real Element of REAL
((i . cij) + (j . cij)) ^2 is V11() V12() ext-real Element of REAL
(i + j) . cij is V11() V12() ext-real Element of REAL
((i + j) . cij) ^2 is V11() V12() ext-real Element of REAL
(sqr (i + j)) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i + j)) is V11() V12() ext-real V89() Element of REAL
dom (f + c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij - (len (sqr (i + j))) is V11() V12() ext-real V89() Element of REAL
((i ^ f) + (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) + (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((f . f) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) + (c₄ . f) is V11() V12() ext-real Element of REAL
((f . f) + (c₄ . f)) ^2 is V11() V12() ext-real Element of REAL
(f + c₄) . f is V11() V12() ext-real Element of REAL
((f + c₄) . f) ^2 is V11() V12() ext-real Element of REAL
(sqr (f + c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i + j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i + j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) + (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (f + c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (f + c₄) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (i + j)) ^ (abs (f + c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs ((i ^ f) + (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) + (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f + c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i + j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i + j))) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i + j))) + (len (abs (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((abs (i + j)) ^ (abs (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(abs ((i ^ f) + (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((abs (i + j)) ^ (abs (f + c₄))) . cij is V11() V12() ext-real Element of REAL
dom (abs ((i ^ f) + (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) + (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs (i + j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) + (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) + (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) + (j . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) + (j . cij)) is V11() V12() ext-real Element of REAL
(i + j) . f is V11() V12() ext-real Element of REAL
abs ((i + j) . f) is V11() V12() ext-real Element of REAL
(abs (i + j)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i + j)) is V11() V12() ext-real V89() Element of REAL
dom (f + c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs (f + c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len (abs (i + j))) is V11() V12() ext-real V89() Element of REAL
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) + (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) + (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((f . f) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) + (c₄ . f) is V11() V12() ext-real Element of REAL
abs ((f . f) + (c₄ . f)) is V11() V12() ext-real Element of REAL
(f + c₄) . f is V11() V12() ext-real Element of REAL
abs ((f + c₄) . f) is V11() V12() ext-real Element of REAL
(abs (f + c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i - j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) - (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (f - c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr (i - j)) ^ (sqr (f - c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr ((i ^ f) - (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) - (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f - c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (i - j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i - j))) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i - j))) + (len (sqr (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((sqr (i - j)) ^ (sqr (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(sqr ((i ^ f) - (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((sqr (i - j)) ^ (sqr (f - c₄))) . cij is V11() V12() ext-real Element of REAL
dom (sqr ((i ^ f) - (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) - (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (sqr (i - j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
((i ^ f) - (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) - (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((i . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) - (j . cij) is V11() V12() ext-real Element of REAL
((i . cij) - (j . cij)) ^2 is V11() V12() ext-real Element of REAL
(i - j) . cij is V11() V12() ext-real Element of REAL
((i - j) . cij) ^2 is V11() V12() ext-real Element of REAL
(sqr (i - j)) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i - j)) is V11() V12() ext-real V89() Element of REAL
dom (f - c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij - (len (sqr (i - j))) is V11() V12() ext-real V89() Element of REAL
((i ^ f) - (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) - (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((f . f) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) - (c₄ . f) is V11() V12() ext-real Element of REAL
((f . f) - (c₄ . f)) ^2 is V11() V12() ext-real Element of REAL
(f - c₄) . f is V11() V12() ext-real Element of REAL
((f - c₄) . f) ^2 is V11() V12() ext-real Element of REAL
(sqr (f - c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i - j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i - j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) - (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (f - c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (f - c₄) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (i - j)) ^ (abs (f - c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs ((i ^ f) - (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) - (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f - c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i - j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i - j))) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i - j))) + (len (abs (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((abs (i - j)) ^ (abs (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(abs ((i ^ f) - (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((abs (i - j)) ^ (abs (f - c₄))) . cij is V11() V12() ext-real Element of REAL
dom (abs ((i ^ f) - (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) - (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs (i - j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) - (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) - (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) - (j . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) - (j . cij)) is V11() V12() ext-real Element of REAL
(i - j) . f is V11() V12() ext-real Element of REAL
abs ((i - j) . f) is V11() V12() ext-real Element of REAL
(abs (i - j)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i - j)) is V11() V12() ext-real V89() Element of REAL
dom (f - c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs (f - c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len (abs (i - j))) is V11() V12() ext-real V89() Element of REAL
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) - (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) - (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((f . f) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) - (c₄ . f) is V11() V12() ext-real Element of REAL
abs ((f . f) - (c₄ . f)) is V11() V12() ext-real Element of REAL
(f - c₄) . f is V11() V12() ext-real Element of REAL
abs ((f - c₄) . f) is V11() V12() ext-real Element of REAL
(abs (f - c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid i is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL i is non empty functional FinSequence-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist i is V16() V19([:(REAL i),(REAL i):]) V20( REAL ) Function-like V30([:(REAL i),(REAL i):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL i),(REAL i):],REAL:]
[:(REAL i),(REAL i):] is non empty V16() set
[:[:(REAL i),(REAL i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL i),(REAL i):],REAL:] is non empty set
MetrStruct(# (REAL i),(Pitag_dist i) #) is strict MetrStruct
the carrier of (Euclid i) is non empty set
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
TOP-REAL i is non empty TopSpace-like V105() V130() V131() V132() V133() V134() V135() V136() V181() L15()
the carrier of (TOP-REAL i) is non empty set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
c₄ is Element of [: the carrier of i, the carrier of j:]
cij is Element of [: the carrier of i, the carrier of j:]
c₄ `1 is Element of the carrier of i
c<sub>4</sub> `2 is Element of the carrier of j
cij `1 is Element of the carrier of i
cij `2 is Element of the carrier of j
the distance of i . ((c₄ `1),(cij `1)) is V11() V12() ext-real Element of REAL
[(c₄ `1),(cij `1)] is V27() set
{(c₄ `1),(cij `1)} is set
{(c₄ `1)} is set
{{(c<sub>4</sub> `1),(cij `1)},{(c<sub>4</sub> `1)}} is set
the distance of i . [(c₄ `1),(cij `1)] is V11() V12() ext-real set
the distance of j . ((c₄ `2),(cij `2)) is V11() V12() ext-real Element of REAL
[(c₄ `2),(cij `2)] is V27() set
{(c₄ `2),(cij `2)} is set
{(c₄ `2)} is set
{{(c<sub>4</sub> `2),(cij `2)},{(c<sub>4</sub> `2)}} is set
the distance of j . [(c₄ `2),(cij `2)] is V11() V12() ext-real set
max (( the distance of i . ((c₄ `1),(cij `1))),( the distance of j . ((c₄ `2),(cij `2)))) is V11() V12() ext-real Element of REAL
[(c₄ `1),(c<sub>4</sub> `2)] is V27() Element of [: the carrier of i, the carrier of j:]
{(c₄ `1),(c<sub>4</sub> `2)} is set
{{(c₄ `1),(c<sub>4</sub> `2)},{(c₄ `1)}} is set
[(cij `1),(cij `2)] is V27() Element of [: the carrier of i, the carrier of j:]
{(cij `1),(cij `2)} is set
{(cij `1)} is set
{{(cij `1),(cij `2)},{(cij `1)}} is set
[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:] is non empty V16() set
[:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:] is non empty set
c<sub>4</sub> is V16() V19([:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:]) V20( REAL ) Function-like V30([:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:], REAL ) complex-yielding V141() V142() Element of bool [:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:]
MetrStruct(# [: the carrier of i, the carrier of j:],c<sub>4</sub> #) is strict MetrStruct
cij is strict MetrStruct
the carrier of cij is set
the distance of cij is V16() V19([: the carrier of cij, the carrier of cij:]) V20( REAL ) Function-like V30([: the carrier of cij, the carrier of cij:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of cij, the carrier of cij:],REAL:]
[: the carrier of cij, the carrier of cij:] is V16() set
[:[: the carrier of cij, the carrier of cij:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of cij, the carrier of cij:],REAL:] is non empty set
f is Element of the carrier of cij
f is Element of the carrier of cij
the distance of cij . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of cij . [f,f] is V11() V12() ext-real set
c<sub>4</sub> . (f,f) is set
c<sub>4</sub> . [f,f] is V11() V12() ext-real set
f is Element of the carrier of i
fj is Element of the carrier of j
[f,fj] is V27() Element of [: the carrier of i, the carrier of j:]
{f,fj} is set
{f} is set
{{f,fj},{f}} is set
fi is Element of the carrier of i
Fi is Element of the carrier of j
[fi,Fi] is V27() Element of [: the carrier of i, the carrier of j:]
{fi,Fi} is set
{fi} is set
{{fi,Fi},{fi}} is set
the distance of i . (f,fi) is V11() V12() ext-real Element of REAL
[f,fi] is V27() set
{f,fi} is set
{{f,fi},{f}} is set
the distance of i . [f,fi] is V11() V12() ext-real set
the distance of j . (fj,Fi) is V11() V12() ext-real Element of REAL
[fj,Fi] is V27() set
{fj,Fi} is set
{fj} is set
{{fj,Fi},{fj}} is set
the distance of j . [fj,Fi] is V11() V12() ext-real set
max (( the distance of i . (f,fi)),( the distance of j . (fj,Fi))) is V11() V12() ext-real Element of REAL
f is strict MetrStruct
the carrier of f is set
the distance of f is V16() V19([: the carrier of f, the carrier of f:]) V20( REAL ) Function-like V30([: the carrier of f, the carrier of f:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of f, the carrier of f:],REAL:]
[: the carrier of f, the carrier of f:] is V16() set
[:[: the carrier of f, the carrier of f:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of f, the carrier of f:],REAL:] is non empty set
c<sub>4</sub> is strict MetrStruct
the carrier of c<sub>4</sub> is set
the distance of c<sub>4</sub> is V16() V19([: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:]) V20( REAL ) Function-like V30([: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:]
[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:] is V16() set
[:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:] is non empty set
f is set
f is set
the distance of f . (f,f) is set
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of f . [f,f] is V11() V12() ext-real set
the distance of c<sub>4</sub> . (f,f) is set
the distance of c<sub>4</sub> . [f,f] is V11() V12() ext-real set
fi is Element of the carrier of i
Fi is Element of the carrier of j
[fi,Fi] is V27() Element of [: the carrier of i, the carrier of j:]
{fi,Fi} is set
{fi} is set
{{fi,Fi},{fi}} is set
fj is Element of the carrier of i
Fj is Element of the carrier of j
[fj,Fj] is V27() Element of [: the carrier of i, the carrier of j:]
{fj,Fj} is set
{fj} is set
{{fj,Fj},{fj}} is set
the distance of i . (fi,fj) is V11() V12() ext-real Element of REAL
[fi,fj] is V27() set
{fi,fj} is set
{{fi,fj},{fi}} is set
the distance of i . [fi,fj] is V11() V12() ext-real set
the distance of j . (Fi,Fj) is V11() V12() ext-real Element of REAL
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
the distance of j . [Fi,Fj] is V11() V12() ext-real set
max (( the distance of i . (fi,fj)),( the distance of j . (Fi,Fj))) is V11() V12() ext-real Element of REAL
r1 is Element of the carrier of i
bb is Element of the carrier of j
[r1,bb] is V27() Element of [: the carrier of i, the carrier of j:]
{r1,bb} is set
{r1} is set
{{r1,bb},{r1}} is set
b is Element of the carrier of i
fb is Element of the carrier of j
[b,fb] is V27() Element of [: the carrier of i, the carrier of j:]
{b,fb} is set
{b} is set
{{b,fb},{b}} is set
the distance of i . (r1,b) is V11() V12() ext-real Element of REAL
[r1,b] is V27() set
{r1,b} is set
{{r1,b},{r1}} is set
the distance of i . [r1,b] is V11() V12() ext-real set
the distance of j . (bb,fb) is V11() V12() ext-real Element of REAL
[bb,fb] is V27() set
{bb,fb} is set
{bb} is set
{{bb,fb},{bb}} is set
the distance of j . [bb,fb] is V11() V12() ext-real set
max (( the distance of i . (r1,b)),( the distance of j . (bb,fb))) is V11() V12() ext-real Element of REAL
i is non empty MetrStruct
j is non empty MetrStruct
(i,j) is strict MetrStruct
the carrier of (i,j) is set
the carrier of i is non empty set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
f is Element of the carrier of i
c<sub>4</sub> is Element of the carrier of j
[f,c<sub>4</sub>] is V27() set
{f,c<sub>4</sub>} is set
{f} is set
{{f,c<sub>4</sub>},{f}} is set
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
[f,c<sub>4</sub>] is V27() Element of [: the carrier of i, the carrier of j:]
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
j is non empty MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
f is Element of the carrier of (i,j)
f `1 is set
the carrier of i is non empty set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
f `2 is set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
(i,j) is non empty strict MetrStruct
f is Element of the carrier of i
c₄ is Element of the carrier of i
dist (f,c₄) is V11() V12() ext-real Element of REAL
the distan