:: GENEALG1 semantic presentation

REAL is set
NAT is non empty V11() V12() V13() Element of K10(REAL)
K10(REAL) is set
NAT is non empty V11() V12() V13() set
K10(NAT) is set
K10(NAT) is set
COMPLEX is set
RAT is set
INT is set
K11(COMPLEX,COMPLEX) is V19() set
K10(K11(COMPLEX,COMPLEX)) is set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is V19() set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is set
K11(REAL,REAL) is V19() set
K10(K11(REAL,REAL)) is set
K11(K11(REAL,REAL),REAL) is V19() set
K10(K11(K11(REAL,REAL),REAL)) is set
K11(RAT,RAT) is V19() set
K10(K11(RAT,RAT)) is set
K11(K11(RAT,RAT),RAT) is V19() set
K10(K11(K11(RAT,RAT),RAT)) is set
K11(INT,INT) is V19() set
K10(K11(INT,INT)) is set
K11(K11(INT,INT),INT) is V19() set
K10(K11(K11(INT,INT),INT)) is set
K11(NAT,NAT) is V19() set
K11(K11(NAT,NAT),NAT) is V19() set
K10(K11(K11(NAT,NAT),NAT)) is set
K265() is set
1 is non empty ext-real V10() V11() V12() V13() V17() V18() Element of NAT
2 is non empty ext-real V10() V11() V12() V13() V17() V18() Element of NAT
3 is non empty ext-real V10() V11() V12() V13() V17() V18() Element of NAT
{} is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered set
0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
n1 is non empty set
n3 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n3 ^ n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n5 is ext-real V10() V11() V12() V13() V17() V18() set
(n3 ^ n4) /^ n5 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n3 /^ n5 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
(n3 /^ n5) ^ n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
len (n3 ^ n4) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n3) + (len n4) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n3 ^ n4) /^ n6 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
len ((n3 ^ n4) /^ n6) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len (n3 ^ n4)) - n6 is ext-real V10() V18() set
n3 /^ n6 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
(n3 /^ n6) ^ n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
len ((n3 /^ n6) ^ n4) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n3 /^ n6) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len (n3 /^ n6)) + (len n4) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n3) - n6 is ext-real V10() V18() set
((len n3) - n6) + (len n4) is ext-real V10() V18() set
((len n3) + (len n4)) - n6 is ext-real V10() V18() set
n2 is ext-real V10() V11() V12() V13() V17() V18() set
((n3 ^ n4) /^ n6) . n2 is set
((n3 /^ n6) ^ n4) . n2 is set
Seg (len ((n3 ^ n4) /^ n6)) is V36() V43( len ((n3 ^ n4) /^ n6)) Element of K10(NAT)
dom ((n3 ^ n4) /^ n6) is Element of K10(NAT)
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
S + n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len n3) is V36() V43( len n3) Element of K10(NAT)
dom n3 is Element of K10(NAT)
Seg (len (n3 /^ n6)) is V36() V43( len (n3 /^ n6)) Element of K10(NAT)
dom (n3 /^ n6) is Element of K10(NAT)
((n3 /^ n6) ^ n4) . S is set
(n3 /^ n6) . S is set
n3 . (S + n6) is set
((n3 ^ n4) /^ n6) . S is set
(n3 ^ n4) . (S + n6) is set
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
((n3 /^ n6) ^ n4) . S is set
S - (len (n3 /^ n6)) is ext-real V10() V18() set
n4 . (S - (len (n3 /^ n6))) is set
S - ((len n3) - n6) is ext-real V10() V18() set
n4 . (S - ((len n3) - n6)) is set
S + n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(S + n6) - (len n3) is ext-real V10() V18() set
n4 . ((S + n6) - (len n3)) is set
((n3 ^ n4) /^ n6) . S is set
(n3 ^ n4) . (S + n6) is set
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n1 is non empty set
n3 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n3 ^ n4 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n3) + n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n3 ^ n4) | ((len n3) + n5) is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n4 | n5 is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
n3 ^ (n4 | n5) is V19() V22( NAT ) V23(n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n1
Seg ((len n3) + n5) is V36() V43((len n3) + n5) Element of K10(NAT)
(n3 ^ n4) | (Seg ((len n3) + n5)) is V19() V22( NAT ) V22( Seg ((len n3) + n5)) V22( NAT ) V23(n1) Function-like FinSubsequence-like Element of K10(K11(NAT,n1))
K11(NAT,n1) is V19() set
K10(K11(NAT,n1)) is set
Seg n5 is V36() V43(n5) Element of K10(NAT)
n4 | (Seg n5) is V19() V22( NAT ) V22( Seg n5) V22( NAT ) V23(n1) Function-like FinSubsequence-like Element of K10(K11(NAT,n1))
n1 is non empty V19() non-empty Function-like set
Union n1 is set
rng n1 is non empty V4() V5() set
union (rng n1) is non empty set
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
len n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len n1) is V36() V43( len n1) Element of K10(NAT)
n3 is ext-real V10() V11() V12() V13() V17() V18() set
n1 . n3 is set
dom n1 is non empty Element of K10(NAT)
n4 is Element of dom n1
n1 . n4 is non empty set
[#] (n1 . n3) is Element of K10((n1 . n3))
K10((n1 . n3)) is set
n5 is Element of n1 . n3
rng n1 is non empty V4() V5() set
union (rng n1) is non empty set
n6 is Element of Union n1
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
dom n3 is Element of K10(NAT)
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 . n4 is set
n1 . n4 is set
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5),(n1,n3,n4,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5) | n6) ^ ((n1,n3,n4,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,(n1,n3,n4,n5,n6),(n1,n4,n3,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6) | n2) ^ ((n1,n4,n3,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5),(n1,n3,n4,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5) | n6) ^ ((n1,n3,n4,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6),(n1,n4,n3,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6) | n2) ^ ((n1,n4,n3,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6),(n1,n3,n4,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6) | n2) ^ ((n1,n3,n4,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,(n1,n3,n4,n5,n6,n2),(n1,n4,n3,n5,n6,n2),S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) | S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) /^ S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2) | S) ^ ((n1,n4,n3,n5,n6,n2) /^ S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5,n6,n2,S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5),(n1,n3,n4,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5) | n6) ^ ((n1,n3,n4,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6),(n1,n4,n3,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6) | n2) ^ ((n1,n4,n3,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6),(n1,n3,n4,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6) | n2) ^ ((n1,n3,n4,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6,n2),(n1,n4,n3,n5,n6,n2),S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) | S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) /^ S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2) | S) ^ ((n1,n4,n3,n5,n6,n2) /^ S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6,n2),(n1,n3,n4,n5,n6,n2),S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) | S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) /^ S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6,n2) | S) ^ ((n1,n3,n4,n5,n6,n2) /^ S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
p1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,(n1,n3,n4,n5,n6,n2,S),(n1,n4,n3,n5,n6,n2,S),p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2,S) | p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S) /^ p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2,S) | p1) ^ ((n1,n4,n3,n5,n6,n2,S) /^ p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
p1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5,n6,n2,S,p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2,S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5),(n1,n3,n4,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5) | n6) ^ ((n1,n3,n4,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6),(n1,n4,n3,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6) | n2) ^ ((n1,n4,n3,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6),(n1,n3,n4,n5,n6),n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6) | n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6) /^ n2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6) | n2) ^ ((n1,n3,n4,n5,n6) /^ n2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6,n2),(n1,n4,n3,n5,n6,n2),S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) | S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) /^ S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2) | S) ^ ((n1,n4,n3,n5,n6,n2) /^ S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6,n2),(n1,n3,n4,n5,n6,n2),S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2) | S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2) /^ S is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6,n2) | S) ^ ((n1,n3,n4,n5,n6,n2) /^ S) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5,n6,n2,S),(n1,n4,n3,n5,n6,n2,S),p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2,S) | p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S) /^ p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2,S) | p1) ^ ((n1,n4,n3,n5,n6,n2,S) /^ p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S,p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n4,n3,n5,n6,n2,S),(n1,n3,n4,n5,n6,n2,S),p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S) | p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2,S) /^ p1 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n4,n3,n5,n6,n2,S) | p1) ^ ((n1,n3,n4,n5,n6,n2,S) /^ p1) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
p2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,(n1,n3,n4,n5,n6,n2,S,p1),(n1,n4,n3,n5,n6,n2,S,p1),p2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5,n6,n2,S,p1) | p2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5,n6,n2,S,p1) /^ p2 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5,n6,n2,S,p1) | p2) ^ ((n1,n4,n3,n5,n6,n2,S,p1) /^ p2) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n3 is non empty set
n4 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n5 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n4 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
len (n3,n4,n5,n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n4 | n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n5 /^ n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len (n4 | n1)) + (len (n5 /^ n1)) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n5) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
(len n3) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
(len n4) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
(len n4) - n1 is ext-real V10() V18() set
n1 + ((len n4) - n1) is ext-real V10() V18() set
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg n1 is V36() V43(n1) Element of K10(NAT)
n4 | (Seg n1) is V19() V22( NAT ) V22( Seg n1) V22( NAT ) V23( Union n3) Function-like FinSubsequence-like Element of K10(K11(NAT,(Union n3)))
K11(NAT,(Union n3)) is V19() set
K10(K11(NAT,(Union n3))) is set
(len n4) - n1 is ext-real V10() V18() set
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n5) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
(len n3) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
(len n4) -' n1 is ext-real non negative V10() V11() V12() V13() V17() V18() Element of NAT
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
dom (n3,n4,n5,n1) is Element of K10(NAT)
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n3,n4,n5,n1) . n6 is set
n3 . n6 is set
dom (n4 | n1) is Element of K10(NAT)
dom n4 is Element of K10(NAT)
(n4 | n1) . n6 is set
(n4 | n1) /. n6 is Element of Union n3
n4 /. n6 is Element of Union n3
n4 . n6 is set
dom (n5 /^ n1) is Element of K10(NAT)
len (n4 | n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n2 is ext-real V10() V11() V12() V13() V17() V18() set
(len (n4 | n1)) + n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n2 is ext-real V10() V11() V12() V13() V17() V18() set
(len (n4 | n1)) + n2 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n1 + S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
dom n5 is Element of K10(NAT)
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len n5) is V36() V43( len n5) Element of K10(NAT)
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n4) - n1 is ext-real V10() V18() set
len (n5 /^ n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len (n5 /^ n1)) is V36() V43( len (n5 /^ n1)) Element of K10(NAT)
1 + n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(len n4) - 1 is ext-real V10() V18() set
(len n4) + 1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n1 + S is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len n3) is V36() V43( len n3) Element of K10(NAT)
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
Seg (len n5) is V36() V43( len n5) Element of K10(NAT)
dom n5 is Element of K10(NAT)
(n5 /^ n1) . S is set
(n5 /^ n1) /. S is Element of Union n3
n5 /. (n1 + S) is Element of Union n3
n5 . (n1 + S) is set
dom (n4 | n1) is Element of K10(NAT)
dom (n5 /^ n1) is Element of K10(NAT)
len (n4 | n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
(n1,n3,n4,0) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n3 | 0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) V23( Union n1) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of Union n1
n4 /^ 0 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | 0) ^ (n4 /^ 0) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n3 is non empty set
n4 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n5 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n4 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n4 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 ^ {} is V19() V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n4 is non empty set
n5 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n6 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n1) ^ (n6 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n1),(n4,n6,n5,n1),n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n1) | n3) ^ ((n4,n6,n5,n1) /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n2 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
S is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n2,S,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n2 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
S /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n2 | n3) ^ (S /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n1 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n1 is non empty set
n3 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n4 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like (n1)
n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n1,n3,n4,n5,n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n3 | n5) ^ (n4 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n4 | n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n3 /^ n5 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n4 | n5) ^ (n3 /^ n5) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,(n1,n3,n4,n5),(n1,n4,n3,n5),n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n3,n4,n5) | n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
(n1,n4,n3,n5) /^ n6 is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
((n1,n3,n4,n5) | n6) ^ ((n1,n4,n3,n5) /^ n6) is V19() V22( NAT ) V23( Union n1) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n1
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n3 is non empty set
n4 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n5 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,0,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 | 0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) V23( Union n3) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of Union n3
n5 /^ 0 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n4 | 0) ^ (n5 /^ 0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 | 0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) V23( Union n3) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of Union n3
n4 /^ 0 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n5 | 0) ^ (n4 /^ 0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,(n3,n4,n5,0),(n3,n5,n4,0),n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n4,n5,0) | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,0) /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
((n3,n4,n5,0) | n1) ^ ((n3,n5,n4,0) /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n5 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n5 | n1) ^ (n4 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n5,(n3,n5,n4,0),n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n5,n4,0) /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n5 | n1) ^ ((n3,n5,n4,0) /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n3 is non empty set
n4 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n5 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1,0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n4 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n5 | n1) ^ (n4 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,(n3,n4,n5,n1),(n3,n5,n4,n1),0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n4,n5,n1) | 0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) V23( Union n3) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of Union n3
(n3,n5,n4,n1) /^ 0 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
((n3,n4,n5,n1) | 0) ^ ((n3,n5,n4,n1) /^ 0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n6 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n2 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n6,n2,0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n6 | 0 is empty ext-real V10() V11() V12() V13() V15() V16() V17() V18() V19() non-empty empty-yielding V22( NAT ) V23( Union n3) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of Union n3
n2 /^ 0 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n6 | 0) ^ (n2 /^ 0) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n4 is non empty set
n5 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n1) ^ (n6 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n1),(n4,n6,n5,n1),n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n1) | n3) ^ ((n4,n6,n5,n1) /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n5 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n3) ^ (n6 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n6 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,(n4,n6,n5,n1),n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n6,n5,n1) /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n3) ^ ((n4,n6,n5,n1) /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n4 is non empty set
n5 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n3,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n3) ^ (n6 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n3) ^ (n5 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n3),(n4,n6,n5,n3),n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3) | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n3) /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n3) | n1) ^ ((n4,n6,n5,n3) /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n4,n5,n6,n3) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n4,n6,n5,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,(n4,n5,n6,n3),(n4,n6,n5,n3),n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n3) | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n3) /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n3) | n1) ^ ((n4,n6,n5,n3) /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n4 is non empty set
n5 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n6 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n1) ^ (n6 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n1),(n4,n6,n5,n1),n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n1) | n3) ^ ((n4,n6,n5,n1) /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n5 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n3) ^ (n6 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n3 is non empty set
n4 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
n5 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n4 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n5 | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n5 | n1) ^ (n4 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,(n3,n4,n5,n1),(n3,n5,n4,n1),n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n4,n5,n1) | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
(n3,n5,n4,n1) /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
((n3,n4,n5,n1) | n1) ^ ((n3,n5,n4,n1) /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
((n5 | n1) ^ (n4 /^ n1)) /^ n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n5 | n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n3,n5,n4,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
len (n3,n5,n4,n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
((n4 | n1) ^ (n5 /^ n1)) | n1 is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len (n4 | n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
len n5 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
(n3,n4,n5,n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like (n3)
len (n3,n4,n5,n1) is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n3) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n3
n4 ^ {} is V19() V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len n4 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n1 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n3 is ext-real V10() V11() V12() V13() V17() V18() Element of NAT
n4 is non empty V19() non-empty V22( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
Union n4 is non empty set
n5 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
n6 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n1) ^ (n6 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n1) ^ (n5 /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n1),(n4,n6,n5,n1),n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n1) | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n1) /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n1) | n3) ^ ((n4,n6,n5,n1) /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3,n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like (n4)
(n4,n5,n6,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n5 | n3) ^ (n6 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n6 | n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
n5 /^ n3 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n6 | n3) ^ (n5 /^ n3) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,(n4,n5,n6,n3),(n4,n6,n5,n3),n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n5,n6,n3) | n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
(n4,n6,n5,n3) /^ n1 is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of Union n4
((n4,n5,n6,n3) | n1) ^ ((n4,n6,n5,n3) /^ n1) is V19() V22( NAT ) V23( Union n4) Function-like V36() FinSequence-like FinSubsequence-like Fi