:: INT_5 semantic presentation

REAL is non empty non trivial non finite V74() V75() V76() V80() set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V74() V75() V76() V77() V78() V79() V80() Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V74() V75() V76() V77() V78() V79() V80() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V74() V80() set
RAT is non empty non trivial non finite V74() V75() V76() V77() V80() set
INT is non empty non trivial non finite V74() V75() V76() V77() V78() V80() set
[:REAL,REAL:] is non empty non trivial V12() non finite V64() V65() V66() set
bool [:REAL,REAL:] is non empty non trivial non finite set
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() set
1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
{0,1} is non empty finite V42() V74() V75() V76() V77() V78() V79() set
K349() is set
bool K349() is non empty set
K350() is Element of bool K349()
2 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
SetPrimes is non empty non trivial non finite V74() V75() V76() V77() V78() V79() Element of bool NAT
K542() is V111() V139() L8()
the U1 of K542() is set
[:NAT,REAL:] is non empty non trivial V12() non finite V64() V65() V66() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial V12() non finite V64() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V12() non finite V64() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial V12() non finite V64() V65() V66() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial V12() V16( RAT ) non finite V64() V65() V66() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial V12() V16( RAT ) non finite V64() V65() V66() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial V12() V16( RAT ) V16( INT ) non finite V64() V65() V66() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial V12() V16( RAT ) V16( INT ) non finite V64() V65() V66() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial V12() V16( RAT ) V16( INT ) non finite V64() V65() V66() V67() set
[:[:NAT,NAT:],NAT:] is non empty non trivial V12() V16( RAT ) V16( INT ) non finite V64() V65() V66() V67() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
3 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V59() V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() Element of NAT
Seg 1 is non empty trivial finite 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
{1} is non empty trivial finite V42() 1 -element V74() V75() V76() V77() V78() V79() set
Seg 2 is non empty finite 2 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
{1,2} is non empty finite V42() V74() V75() V76() V77() V78() V79() set
- 1 is V11() integer V55() ext-real non positive set
card 0 is empty V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() set
7 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
4 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
5 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
6 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
{0} is non empty trivial functional finite V42() 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
<*> REAL is empty proper V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( REAL ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() FinSequence of REAL
Sum (<*> REAL) is V11() V55() ext-real Element of REAL
Product (<*> REAL) is V11() V55() ext-real Element of REAL
union 0 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
p is V11() integer V55() ext-real set
q is V11() integer V55() ext-real set
p is V11() integer V55() ext-real set
q - p is V11() integer V55() ext-real set
- p is V11() integer V55() ext-real set
q + (- p) is V11() integer V55() ext-real set
q is V11() integer V55() ext-real set
p * q is V11() integer V55() ext-real set
p9 is V11() integer V55() ext-real set
p * p9 is V11() integer V55() ext-real set
q - p9 is V11() integer V55() ext-real set
- p9 is V11() integer V55() ext-real set
q + (- p9) is V11() integer V55() ext-real set
p * (q - p9) is V11() integer V55() ext-real set
p is V11() integer V55() ext-real set
q is V11() integer V55() ext-real set
p is V11() integer V55() ext-real set
q - p is V11() integer V55() ext-real set
- p is V11() integer V55() ext-real set
q + (- p) is V11() integer V55() ext-real set
- (q - p) is V11() integer V55() ext-real set
(- (q - p)) + q is V11() integer V55() ext-real set
p is V11() integer V55() ext-real set
q is V11() integer V55() ext-real set
q mod p is V11() integer V55() ext-real set
p is V11() integer V55() ext-real set
p * p is V11() integer V55() ext-real set
(p * p) + 0 is V11() integer V55() ext-real set
((p * p) + 0) mod p is V11() integer V55() ext-real set
0 mod p is V11() integer V55() ext-real set
q div p is V11() integer V55() ext-real set
q / p is V11() V55() ext-real set
p " is V11() V55() ext-real set
q * (p ") is V11() V55() ext-real set
[\(q / p)/] is V11() integer V55() ext-real set
(q div p) * p is V11() integer V55() ext-real set
((q div p) * p) + (q mod p) is V11() integer V55() ext-real set
p is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q is V11() integer V55() ext-real V59() Element of INT
p is V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V109() set
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom p is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
p . q is set
p . q is V11() integer V55() ext-real set
q -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q |^ (q -' 1) is V11() integer V55() ext-real set
(p . q) * (q |^ (q -' 1)) is V11() integer V55() ext-real set
q is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
Sum q is V11() integer V55() ext-real V59() Element of INT
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom q is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
p9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
q . p9 is V11() integer V55() ext-real set
p . p9 is V11() integer V55() ext-real set
p9 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q |^ (p9 -' 1) is V11() integer V55() ext-real set
(p . p9) * (q |^ (p9 -' 1)) is V11() integer V55() ext-real set
q is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
p is V11() integer V55() ext-real V59() Element of INT
q . p is V11() integer V55() ext-real V59() Element of INT
q is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
p is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
q is V11() integer V55() ext-real V59() Element of INT
q . q is V11() integer V55() ext-real V59() Element of INT
p . q is V11() integer V55() ext-real V59() Element of INT
p9 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len p9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom p9 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum p9 is V11() integer V55() ext-real V59() Element of INT
f1 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len f1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom f1 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum f1 is V11() integer V55() ext-real V59() Element of INT
q9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
p9 . q9 is V11() integer V55() ext-real set
f1 . q9 is V11() integer V55() ext-real set
p . q9 is V11() integer V55() ext-real set
q9 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q |^ (q9 -' 1) is V11() integer V55() ext-real set
(p . q9) * (q |^ (q9 -' 1)) is V11() integer V55() ext-real set
p is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(p) is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
p . 1 is V11() integer V55() ext-real set
INT --> (p . 1) is V12() V15( INT ) V16( INT ) V16({(p . 1)}) Function-like V26( INT ,{(p . 1)}) V64() V65() V66() Element of bool [:INT,{(p . 1)}:]
{(p . 1)} is non empty trivial finite 1 -element V74() V75() V76() V77() V78() set
[:INT,{(p . 1)}:] is non empty non trivial V12() V16( RAT ) V16( INT ) non finite V64() V65() V66() set
bool [:INT,{(p . 1)}:] is non empty non trivial non finite set
dom (p) is V74() V75() V76() V77() V78() Element of bool INT
bool INT is non empty non trivial non finite set
q is set
(p) . q is V11() integer V55() ext-real set
p is V11() integer V55() ext-real V59() Element of INT
(p) . p is V11() integer V55() ext-real V59() Element of INT
q is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom q is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum q is V11() integer V55() ext-real V59() Element of INT
q . 1 is V11() integer V55() ext-real set
1 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p |^ (1 -' 1) is V11() integer V55() ext-real set
(p . 1) * (p |^ (1 -' 1)) is V11() integer V55() ext-real set
p |^ 0 is V11() integer V55() ext-real set
(p . 1) * (p |^ 0) is V11() integer V55() ext-real set
(p . 1) * 1 is V11() integer V55() ext-real set
<*(q . 1)*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
(dom (p)) --> (p . 1) is V12() V15( dom (p)) V16( INT ) V16({(p . 1)}) Function-like V26( dom (p),{(p . 1)}) V64() V65() V66() Element of bool [:(dom (p)),{(p . 1)}:]
[:(dom (p)),{(p . 1)}:] is V12() V16( RAT ) V16( INT ) V64() V65() V66() set
bool [:(dom (p)),{(p . 1)}:] is non empty set
p is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(p) is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
p . 1 is V11() integer V55() ext-real set
q is V11() integer V55() ext-real V59() Element of INT
(p) . q is V11() integer V55() ext-real V59() Element of INT
p is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom p is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum p is V11() integer V55() ext-real V59() Element of INT
p . 1 is V11() integer V55() ext-real set
1 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q |^ (1 -' 1) is V11() integer V55() ext-real set
(p . 1) * (q |^ (1 -' 1)) is V11() integer V55() ext-real set
q |^ 0 is V11() integer V55() ext-real set
(p . 1) * (q |^ 0) is V11() integer V55() ext-real set
(p . 1) * 1 is V11() integer V55() ext-real set
<*(p . 1)*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
p + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
q + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(q + 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom p is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
(len p) - 1 is V11() integer V55() ext-real set
(len p) + (- 1) is V11() integer V55() ext-real set
Sum p is V11() V55() ext-real Element of REAL
q is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q . ((q + 1) + 1) is V11() V55() ext-real set
p9 is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len p9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p9 . 1 is V11() V55() ext-real set
(q + 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg (q + 1) is non empty finite q + 1 -element q + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
q | (Seg (q + 1)) is V12() V15( NAT ) V15( Seg (q + 1)) V15( NAT ) V16( REAL ) Function-like finite FinSubsequence-like V64() V65() V66() V109() Element of bool [:NAT,REAL:]
q9 is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p9 | (Seg (q + 1)) is V12() V15( NAT ) V15( Seg (q + 1)) V15( NAT ) V16( REAL ) Function-like finite FinSubsequence-like V64() V65() V66() V109() Element of bool [:NAT,REAL:]
g1 is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
p9 . ((q + 1) + 1) is V11() V55() ext-real set
<*(p9 . ((q + 1) + 1))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
g1 ^ <*(p9 . ((q + 1) + 1))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
len g1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom g1 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
g1 . 1 is V11() V55() ext-real set
q . ((q + 1) + 1) is V11() V55() ext-real set
<*(q . ((q + 1) + 1))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
q9 ^ <*(q . ((q + 1) + 1))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
Seg ((q + 1) + 1) is non empty finite (q + 1) + 1 -element (q + 1) + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
p . ((q + 1) + 1) is V11() V55() ext-real set
(q . ((q + 1) + 1)) - (p9 . ((q + 1) + 1)) is V11() V55() ext-real set
- (p9 . ((q + 1) + 1)) is V11() V55() ext-real set
(q . ((q + 1) + 1)) + (- (p9 . ((q + 1) + 1))) is V11() V55() ext-real set
p | (Seg (q + 1)) is V12() V15( NAT ) V15( Seg (q + 1)) V15( NAT ) V16( REAL ) Function-like finite FinSubsequence-like V64() V65() V66() V109() Element of bool [:NAT,REAL:]
g4 is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
dom g4 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
len g4 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
<*(p . ((q + 1) + 1))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
g4 ^ <*(p . ((q + 1) + 1))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
g4 . XX is V11() V55() ext-real set
q9 . XX is V11() V55() ext-real set
g1 . XX is V11() V55() ext-real set
(q9 . XX) - (g1 . XX) is V11() V55() ext-real set
- (g1 . XX) is V11() V55() ext-real set
(q9 . XX) + (- (g1 . XX)) is V11() V55() ext-real set
dom q9 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
q . XX is V11() V55() ext-real set
p . XX is V11() V55() ext-real set
p9 . XX is V11() V55() ext-real set
(q . XX) - (p9 . XX) is V11() V55() ext-real set
- (p9 . XX) is V11() V55() ext-real set
(q . XX) + (- (p9 . XX)) is V11() V55() ext-real set
dom q9 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
q9 . (q + 1) is V11() V55() ext-real set
q . (q + 1) is V11() V55() ext-real set
(len g4) - 1 is V11() integer V55() ext-real set
(len g4) + (- 1) is V11() integer V55() ext-real set
Sum g4 is V11() V55() ext-real Element of REAL
XX is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom XX is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum XX is V11() V55() ext-real Element of REAL
(Sum XX) + (q . (q + 1)) is V11() V55() ext-real set
((Sum XX) + (q . (q + 1))) - (p9 . 1) is V11() V55() ext-real set
- (p9 . 1) is V11() V55() ext-real set
((Sum XX) + (q . (q + 1))) + (- (p9 . 1)) is V11() V55() ext-real set
q + 2 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p9 . (q + 2) is V11() V55() ext-real set
(q . (q + 1)) - (p9 . (q + 2)) is V11() V55() ext-real set
- (p9 . (q + 2)) is V11() V55() ext-real set
(q . (q + 1)) + (- (p9 . (q + 2))) is V11() V55() ext-real set
<*((q . (q + 1)) - (p9 . (q + 2)))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
XX ^ <*((q . (q + 1)) - (p9 . (q + 2)))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
f1 is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
len f1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom f1 is non empty finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum f1 is V11() V55() ext-real Element of REAL
(Sum f1) + (q . ((q + 1) + 1)) is V11() V55() ext-real set
((Sum f1) + (q . ((q + 1) + 1))) - (p9 . 1) is V11() V55() ext-real set
((Sum f1) + (q . ((q + 1) + 1))) + (- (p9 . 1)) is V11() V55() ext-real set
(((Sum XX) + (q . (q + 1))) - (p9 . 1)) + (p . ((q + 1) + 1)) is V11() V55() ext-real set
(Sum XX) + ((q . (q + 1)) - (p9 . (q + 2))) is V11() V55() ext-real set
((Sum XX) + ((q . (q + 1)) - (p9 . (q + 2)))) + (q . ((q + 1) + 1)) is V11() V55() ext-real set
(((Sum XX) + ((q . (q + 1)) - (p9 . (q + 2)))) + (q . ((q + 1) + 1))) - (p9 . 1) is V11() V55() ext-real set
(((Sum XX) + ((q . (q + 1)) - (p9 . (q + 2)))) + (q . ((q + 1) + 1))) + (- (p9 . 1)) is V11() V55() ext-real set
f2 is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
Sum f2 is V11() V55() ext-real Element of REAL
(Sum f2) + (q . ((q + 1) + 1)) is V11() V55() ext-real set
((Sum f2) + (q . ((q + 1) + 1))) - (p9 . 1) is V11() V55() ext-real set
((Sum f2) + (q . ((q + 1) + 1))) + (- (p9 . 1)) is V11() V55() ext-real set
(len XX) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom f2 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
n2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
f2 . n2 is V11() V55() ext-real set
q . n2 is V11() V55() ext-real set
n2 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p9 . (n2 + 1) is V11() V55() ext-real set
(q . n2) - (p9 . (n2 + 1)) is V11() V55() ext-real set
- (p9 . (n2 + 1)) is V11() V55() ext-real set
(q . n2) + (- (p9 . (n2 + 1))) is V11() V55() ext-real set
len f2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg (len f2) is finite len f2 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
Seg ((len XX) + 1) is non empty finite (len XX) + 1 -element (len XX) + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
(len XX) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg (len XX) is finite len XX -element V74() V75() V76() V77() V78() V79() Element of bool NAT
{((len XX) + 1)} is non empty trivial finite V42() 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
(Seg (len XX)) \/ {((len XX) + 1)} is non empty finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Seg (len g1) is finite len g1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
q9 . n2 is V11() V55() ext-real set
XX . n2 is V11() V55() ext-real set
g1 . (n2 + 1) is V11() V55() ext-real set
(q9 . n2) - (g1 . (n2 + 1)) is V11() V55() ext-real set
- (g1 . (n2 + 1)) is V11() V55() ext-real set
(q9 . n2) + (- (g1 . (n2 + 1))) is V11() V55() ext-real set
dom <*((q . (q + 1)) - (p9 . (q + 2)))*> is non empty trivial finite 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
<*((q . (q + 1)) - (p9 . (q + 2)))*> . 1 is V11() V55() ext-real set
len f2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
n2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
f1 . n2 is V11() V55() ext-real set
q . n2 is V11() V55() ext-real set
n2 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p9 . (n2 + 1) is V11() V55() ext-real set
(q . n2) - (p9 . (n2 + 1)) is V11() V55() ext-real set
- (p9 . (n2 + 1)) is V11() V55() ext-real set
(q . n2) + (- (p9 . (n2 + 1))) is V11() V55() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom q is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
(len q) - 1 is V11() integer V55() ext-real set
(len q) + (- 1) is V11() integer V55() ext-real set
Sum q is V11() V55() ext-real Element of REAL
p is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p . (0 + 1) is V11() V55() ext-real set
q is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q . 1 is V11() V55() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
len (<*> REAL) is empty V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V59() V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() Element of NAT
dom (<*> REAL) is empty proper V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() Element of bool NAT
(Sum (<*> REAL)) + (p . (0 + 1)) is V11() V55() ext-real set
((Sum (<*> REAL)) + (p . (0 + 1))) - (q . 1) is V11() V55() ext-real set
- (q . 1) is V11() V55() ext-real set
((Sum (<*> REAL)) + (p . (0 + 1))) + (- (q . 1)) is V11() V55() ext-real set
Seg (0 + 1) is non empty finite 0 + 1 -element 0 + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
q . 1 is V11() V55() ext-real set
p . 1 is V11() V55() ext-real set
(p . 1) - (q . 1) is V11() V55() ext-real set
(p . 1) + (- (q . 1)) is V11() V55() ext-real set
<*((p . 1) - (q . 1))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
p9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
(<*> REAL) . p9 is empty V4() V5() V6() V8() V9() V10() V11() V12() non-empty empty-yielding V15( NAT ) V16( RAT ) Function-like one-to-one constant functional integer finite finite-yielding V42() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V55() ext-real non positive non negative V64() V65() V66() V67() V74() V75() V76() V77() V78() V79() V80() V108() V109() set
p . p9 is V11() V55() ext-real set
p9 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q . (p9 + 1) is V11() V55() ext-real set
(p . p9) - (q . (p9 + 1)) is V11() V55() ext-real set
- (q . (p9 + 1)) is V11() V55() ext-real set
(p . p9) + (- (q . (p9 + 1))) is V11() V55() ext-real set
q is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom q is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
(len q) - 1 is V11() integer V55() ext-real set
(len q) + (- 1) is V11() integer V55() ext-real set
Sum q is V11() V55() ext-real Element of REAL
p . (p + 1) is V11() V55() ext-real set
q . 1 is V11() V55() ext-real set
p is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
p + 2 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
p + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(q) is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
q . (p + 2) is V11() integer V55() ext-real set
(p + 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg ((p + 1) + 1) is non empty finite (p + 1) + 1 -element (p + 1) + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
(p + 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom q is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
p9 is V11() integer V55() ext-real set
q is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
f1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(p + 2) - f1 is V11() integer V55() ext-real set
- f1 is V11() integer V55() ext-real non positive set
(p + 2) + (- f1) is V11() integer V55() ext-real set
q . ((p + 2) - f1) is V11() integer V55() ext-real set
q9 is V11() integer V55() ext-real V59() Element of INT
p9 * q9 is V11() integer V55() ext-real set
(q . ((p + 2) - f1)) + (p9 * q9) is V11() integer V55() ext-real set
g1 is V11() integer V55() ext-real V59() Element of INT
p is V11() integer V55() ext-real V59() Element of INT
f1 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len f1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
f1 . 1 is V11() integer V55() ext-real set
Rev f1 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
q9 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len q9 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(q9) is V12() V15( INT ) V16( INT ) Function-like V26( INT , INT ) V64() V65() V66() Element of bool [:INT,INT:]
q9 . (p + 1) is V11() integer V55() ext-real set
q . 1 is V11() integer V55() ext-real set
q9 . 1 is V11() integer V55() ext-real set
p9 * (q9 . 1) is V11() integer V55() ext-real set
(q . 1) + (p9 * (q9 . 1)) is V11() integer V55() ext-real set
g1 is V11() integer V55() ext-real set
g1 is V11() integer V55() ext-real V59() Element of INT
(q) . g1 is V11() integer V55() ext-real V59() Element of INT
g1 - p9 is V11() integer V55() ext-real set
- p9 is V11() integer V55() ext-real set
g1 + (- p9) is V11() integer V55() ext-real set
(q9) . g1 is V11() integer V55() ext-real V59() Element of INT
(g1 - p9) * ((q9) . g1) is V11() integer V55() ext-real set
((g1 - p9) * ((q9) . g1)) + g1 is V11() integer V55() ext-real set
g3 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len g3 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom g3 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum g3 is V11() integer V55() ext-real V59() Element of INT
g3 . (p + 2) is V11() integer V55() ext-real set
((p + 1) + 1) -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ (((p + 1) + 1) -' 1) is V11() integer V55() ext-real set
(q . (p + 2)) * (g1 |^ (((p + 1) + 1) -' 1)) is V11() integer V55() ext-real set
g1 |^ (p + 1) is V11() integer V55() ext-real set
(q . (p + 2)) * (g1 |^ (p + 1)) is V11() integer V55() ext-real set
g3 . 1 is V11() integer V55() ext-real set
1 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ (1 -' 1) is V11() integer V55() ext-real set
(q . 1) * (g1 |^ (1 -' 1)) is V11() integer V55() ext-real set
g1 |^ 0 is V11() integer V55() ext-real set
(q . 1) * (g1 |^ 0) is V11() integer V55() ext-real set
(q . 1) * 1 is V11() integer V55() ext-real set
g4 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g4 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
XX is V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V109() set
len XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom XX is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
f1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
XX . f1 is set
f2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
XX . f2 is set
q9 . f2 is V11() integer V55() ext-real set
g1 |^ f2 is V11() integer V55() ext-real set
(q9 . f2) * (g1 |^ f2) is V11() integer V55() ext-real set
XX . (g4 + 1) is set
q9 . (g4 + 1) is V11() integer V55() ext-real set
g1 |^ (g4 + 1) is V11() integer V55() ext-real set
(q9 . (g4 + 1)) * (g1 |^ (g4 + 1)) is V11() integer V55() ext-real set
g4 + 2 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
q . (g4 + 2) is V11() integer V55() ext-real set
(q . (g4 + 2)) * (g1 |^ (g4 + 1)) is V11() integer V55() ext-real set
f2 is V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V109() set
len f2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom f2 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
n2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
f2 . n2 is set
q9 . n2 is V11() integer V55() ext-real set
p9 * (q9 . n2) is V11() integer V55() ext-real set
n2 -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ (n2 -' 1) is V11() integer V55() ext-real set
(p9 * (q9 . n2)) * (g1 |^ (n2 -' 1)) is V11() integer V55() ext-real set
f2 . 1 is set
(p9 * (q9 . 1)) * (g1 |^ (1 -' 1)) is V11() integer V55() ext-real set
(p9 * (q9 . 1)) * (g1 |^ 0) is V11() integer V55() ext-real set
(p9 * (q9 . 1)) * 1 is V11() integer V55() ext-real set
f1 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
g2 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
len g2 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom g2 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum g2 is V11() integer V55() ext-real V59() Element of INT
(g1 - p9) * g2 is V12() V15( NAT ) V16( REAL ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
dom ((g1 - p9) * g2) is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
len ((g1 - p9) * g2) is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom f1 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
((g1 - p9) * g2) . XX is V11() integer V55() ext-real set
q9 . XX is V11() integer V55() ext-real set
g1 |^ XX is V11() integer V55() ext-real set
(q9 . XX) * (g1 |^ XX) is V11() integer V55() ext-real set
p9 * (q9 . XX) is V11() integer V55() ext-real set
XX -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ (XX -' 1) is V11() integer V55() ext-real set
(p9 * (q9 . XX)) * (g1 |^ (XX -' 1)) is V11() integer V55() ext-real set
((q9 . XX) * (g1 |^ XX)) - ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1))) is V11() integer V55() ext-real set
- ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1))) is V11() integer V55() ext-real set
((q9 . XX) * (g1 |^ XX)) + (- ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1)))) is V11() integer V55() ext-real set
g2 . XX is V11() integer V55() ext-real set
(g1 - p9) * (g2 . XX) is V11() integer V55() ext-real set
(q9 . XX) * (g1 |^ (XX -' 1)) is V11() integer V55() ext-real set
(g1 - p9) * ((q9 . XX) * (g1 |^ (XX -' 1))) is V11() integer V55() ext-real set
(g1 |^ (XX -' 1)) * g1 is V11() integer V55() ext-real set
(q9 . XX) * ((g1 |^ (XX -' 1)) * g1) is V11() integer V55() ext-real set
((q9 . XX) * ((g1 |^ (XX -' 1)) * g1)) - ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1))) is V11() integer V55() ext-real set
((q9 . XX) * ((g1 |^ (XX -' 1)) * g1)) + (- ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1)))) is V11() integer V55() ext-real set
(XX -' 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ ((XX -' 1) + 1) is V11() integer V55() ext-real set
(q9 . XX) * (g1 |^ ((XX -' 1) + 1)) is V11() integer V55() ext-real set
((q9 . XX) * (g1 |^ ((XX -' 1) + 1))) - ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1))) is V11() integer V55() ext-real set
((q9 . XX) * (g1 |^ ((XX -' 1) + 1))) + (- ((p9 * (q9 . XX)) * (g1 |^ (XX -' 1)))) is V11() integer V55() ext-real set
n2 is V12() V15( NAT ) V16( INT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of INT
dom n2 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
((g1 - p9) * g2) . XX is V11() integer V55() ext-real set
f1 . XX is V11() integer V55() ext-real set
n2 . XX is V11() integer V55() ext-real set
(f1 . XX) - (n2 . XX) is V11() integer V55() ext-real set
- (n2 . XX) is V11() integer V55() ext-real set
(f1 . XX) + (- (n2 . XX)) is V11() integer V55() ext-real set
q9 . XX is V11() integer V55() ext-real set
p9 * (q9 . XX) is V11() integer V55() ext-real set
XX -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ (XX -' 1) is V11() integer V55() ext-real set
(p9 * (q9 . XX)) * (g1 |^ (XX -' 1)) is V11() integer V55() ext-real set
g1 |^ XX is V11() integer V55() ext-real set
(q9 . XX) * (g1 |^ XX) is V11() integer V55() ext-real set
(len ((g1 - p9) * g2)) - 1 is V11() integer V55() ext-real set
(len ((g1 - p9) * g2)) + (- 1) is V11() integer V55() ext-real set
Sum ((g1 - p9) * g2) is V11() V55() ext-real Element of REAL
f1 . (g4 + 1) is V11() integer V55() ext-real set
n2 . 1 is V11() integer V55() ext-real set
XX is V12() V15( NAT ) V16( REAL ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() FinSequence of REAL
len XX is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
dom XX is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Sum XX is V11() V55() ext-real Element of REAL
(Sum XX) + (f1 . (g4 + 1)) is V11() V55() ext-real set
((Sum XX) + (f1 . (g4 + 1))) - (n2 . 1) is V11() V55() ext-real set
- (n2 . 1) is V11() integer V55() ext-real set
((Sum XX) + (f1 . (g4 + 1))) + (- (n2 . 1)) is V11() V55() ext-real set
mm is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
XX . mm is V11() V55() ext-real set
mm + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g3 . (mm + 1) is V11() integer V55() ext-real set
dom f1 is finite V74() V75() V76() V77() V78() V79() Element of bool NAT
Seg g4 is finite g4 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
g4 - mm is V11() integer V55() ext-real set
- mm is V11() integer V55() ext-real non positive set
g4 + (- mm) is V11() integer V55() ext-real set
(g4 - mm) + 1 is V11() integer V55() ext-real set
g4 - 1 is V11() integer V55() ext-real set
g4 + (- 1) is V11() integer V55() ext-real set
YY is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(g4 - 1) + 1 is V11() integer V55() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
YY + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
f1 . (YY + 1) is V11() integer V55() ext-real set
(g4 + 2) - YY is V11() integer V55() ext-real set
- YY is V11() integer V55() ext-real non positive set
(g4 + 2) + (- YY) is V11() integer V55() ext-real set
q . ((g4 + 2) - YY) is V11() integer V55() ext-real set
f1 . YY is V11() integer V55() ext-real set
p9 * (f1 . YY) is V11() integer V55() ext-real set
(q . ((g4 + 2) - YY)) + (p9 * (f1 . YY)) is V11() integer V55() ext-real set
Seg (g4 + 1) is non empty finite g4 + 1 -element g4 + 1 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
g4 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
mm + 0 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg (g4 + 2) is non empty finite g4 + 2 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
f1 . mm is V11() integer V55() ext-real set
n2 . (mm + 1) is V11() integer V55() ext-real set
(f1 . mm) - (n2 . (mm + 1)) is V11() integer V55() ext-real set
- (n2 . (mm + 1)) is V11() integer V55() ext-real set
(f1 . mm) + (- (n2 . (mm + 1))) is V11() integer V55() ext-real set
q9 . mm is V11() integer V55() ext-real set
g1 |^ mm is V11() integer V55() ext-real set
(q9 . mm) * (g1 |^ mm) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) - (n2 . (mm + 1)) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) + (- (n2 . (mm + 1))) is V11() integer V55() ext-real set
q9 . (mm + 1) is V11() integer V55() ext-real set
p9 * (q9 . (mm + 1)) is V11() integer V55() ext-real set
(mm + 1) -' 1 is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
g1 |^ ((mm + 1) -' 1) is V11() integer V55() ext-real set
(p9 * (q9 . (mm + 1))) * (g1 |^ ((mm + 1) -' 1)) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) - ((p9 * (q9 . (mm + 1))) * (g1 |^ ((mm + 1) -' 1))) is V11() integer V55() ext-real set
- ((p9 * (q9 . (mm + 1))) * (g1 |^ ((mm + 1) -' 1))) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) + (- ((p9 * (q9 . (mm + 1))) * (g1 |^ ((mm + 1) -' 1)))) is V11() integer V55() ext-real set
(p9 * (q9 . (mm + 1))) * (g1 |^ mm) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) - ((p9 * (q9 . (mm + 1))) * (g1 |^ mm)) is V11() integer V55() ext-real set
- ((p9 * (q9 . (mm + 1))) * (g1 |^ mm)) is V11() integer V55() ext-real set
((q9 . mm) * (g1 |^ mm)) + (- ((p9 * (q9 . (mm + 1))) * (g1 |^ mm))) is V11() integer V55() ext-real set
(q9 . mm) - (p9 * (q9 . (mm + 1))) is V11() integer V55() ext-real set
- (p9 * (q9 . (mm + 1))) is V11() integer V55() ext-real set
(q9 . mm) + (- (p9 * (q9 . (mm + 1)))) is V11() integer V55() ext-real set
((q9 . mm) - (p9 * (q9 . (mm + 1)))) * (g1 |^ mm) is V11() integer V55() ext-real set
(g4 + 1) - mm is V11() integer V55() ext-real set
(g4 + 1) + (- mm) is V11() integer V55() ext-real set
((g4 + 1) - mm) + 1 is V11() integer V55() ext-real set
f1 . (((g4 + 1) - mm) + 1) is V11() integer V55() ext-real set
(f1 . (((g4 + 1) - mm) + 1)) - (p9 * (q9 . (mm + 1))) is V11() integer V55() ext-real set
(f1 . (((g4 + 1) - mm) + 1)) + (- (p9 * (q9 . (mm + 1)))) is V11() integer V55() ext-real set
((f1 . (((g4 + 1) - mm) + 1)) - (p9 * (q9 . (mm + 1)))) * (g1 |^ mm) is V11() integer V55() ext-real set
((g4 - mm) + 1) + 1 is V11() integer V55() ext-real set
f1 . (((g4 - mm) + 1) + 1) is V11() integer V55() ext-real set
(g4 + 1) - (mm + 1) is V11() integer V55() ext-real set
- (mm + 1) is V11() integer V55() ext-real non positive set
(g4 + 1) + (- (mm + 1)) is V11() integer V55() ext-real set
((g4 + 1) - (mm + 1)) + 1 is V11() integer V55() ext-real set
f1 . (((g4 + 1) - (mm + 1)) + 1) is V11() integer V55() ext-real set
p9 * (f1 . (((g4 + 1) - (mm + 1)) + 1)) is V11() integer V55() ext-real set
(f1 . (((g4 - mm) + 1) + 1)) - (p9 * (f1 . (((g4 + 1) - (mm + 1)) + 1))) is V11() integer V55() ext-real set
- (p9 * (f1 . (((g4 + 1) - (mm + 1)) + 1))) is V11() integer V55() ext-real set
(f1 . (((g4 - mm) + 1) + 1)) + (- (p9 * (f1 . (((g4 + 1) - (mm + 1)) + 1)))) is V11() integer V55() ext-real set
((f1 . (((g4 - mm) + 1) + 1)) - (p9 * (f1 . (((g4 + 1) - (mm + 1)) + 1)))) * (g1 |^ mm) is V11() integer V55() ext-real set
q . (mm + 1) is V11() integer V55() ext-real set
(q . (mm + 1)) * (g1 |^ ((mm + 1) -' 1)) is V11() integer V55() ext-real set
<*(g3 . 1)*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
<*(g3 . 1)*> ^ XX is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
g3 . (g4 + 2) is V11() integer V55() ext-real set
<*(g3 . (g4 + 2))*> is non empty trivial V12() V15( NAT ) Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V64() V65() V66() V68() V69() V70() V71() V109() set
(<*(g3 . 1)*> ^ XX) ^ <*(g3 . (g4 + 2))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
YY is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative set
g3 . YY is V11() integer V55() ext-real set
((<*(g3 . 1)*> ^ XX) ^ <*(g3 . (g4 + 2))*>) . YY is V11() V55() ext-real set
XX ^ <*(g3 . (g4 + 2))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
<*(g3 . 1)*> ^ (XX ^ <*(g3 . (g4 + 2))*>) is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
(<*(g3 . 1)*> ^ (XX ^ <*(g3 . (g4 + 2))*>)) . 1 is V11() V55() ext-real set
YY - 1 is V11() integer V55() ext-real set
YY + (- 1) is V11() integer V55() ext-real set
(g4 + 2) - 1 is V11() integer V55() ext-real set
(g4 + 2) + (- 1) is V11() integer V55() ext-real set
(g4 + 1) - 1 is V11() integer V55() ext-real set
(g4 + 1) + (- 1) is V11() integer V55() ext-real set
0 + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
N is V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
Seg g4 is finite g4 -element V74() V75() V76() V77() V78() V79() Element of bool NAT
XX ^ <*(g3 . (g4 + 2))*> is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
dom (XX ^ <*(g3 . (g4 + 2))*>) is non empty finite V74() V75() V76() V77() V78() V79() Element of bool NAT
<*(g3 . 1)*> ^ (XX ^ <*(g3 . (g4 + 2))*>) is non empty V12() V15( NAT ) Function-like finite FinSequence-like FinSubsequence-like V64() V65() V66() V109() set
N + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
(<*(g3 . 1)*> ^ (XX ^ <*(g3 . (g4 + 2))*>)) . (N + 1) is V11() V55() ext-real set
(XX ^ <*(g3 . (g4 + 2))*>) . N is V11() V55() ext-real set
XX . N is V11() V55() ext-real set
g3 . (N + 1) is V11() integer V55() ext-real set
(g4 + 1) + 1 is non empty V4() V5() V6() V10() V11() integer finite cardinal V55() ext-real positive non negative V59() V74() V75() V76() V77() V78() V79() Element of NAT
((<*(g3 . 1)*> ^ XX) ^ <*(g3 . (g4 + 2))*>) . ((g4 + 1) + 1) is V11() V55() ext-real