:: FUNCT_7 semantic presentation

REAL is set
NAT is non empty V18() V19() V20() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty V18() V19() V20() non finite cardinal limit_cardinal set
bool NAT is non empty non finite set
bool NAT is non empty non finite set
COMPLEX is set
RAT is set
INT is set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
2 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
3 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty set
proj1 {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V92() set
proj2 {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
card {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
{{}} is non empty trivial functional 1 -element set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 3 is non empty finite 3 -element Element of bool NAT
{1,2,3} is non empty set
I is Relation-like Function-like set
proj2 I is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
I (#) (id X) is Relation-like X -valued Function-like set
proj1 I is set
[:(proj1 I),X:] is Relation-like set
bool [:(proj1 I),X:] is non empty set
l1 is Relation-like proj1 I -defined X -valued Function-like quasi_total Element of bool [:(proj1 I),X:]
(id X) * l1 is Relation-like proj1 I -defined X -valued Function-like quasi_total Element of bool [:(proj1 I),X:]
I is set
bool I is non empty set
X is non empty set
[:I,X:] is Relation-like set
bool [:I,X:] is non empty set
bool X is non empty set
l1 is Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l2 is Element of bool I
l1 .: l2 is Element of bool X
i1 is Element of bool X
l1 " i1 is Element of bool I
l1 " (l1 .: l2) is Element of bool I
I is non empty set
X is non empty set
[:I,X:] is non empty Relation-like set
bool [:I,X:] is non empty set
bool I is non empty set
l1 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l2 is Element of I
l1 . l2 is Element of X
i1 is Element of bool I
l1 .: i1 is Element of bool X
bool X is non empty set
i2 is Element of I
l1 . i2 is Element of X
I is non empty set
X is non empty set
[:I,X:] is non empty Relation-like set
bool [:I,X:] is non empty set
bool I is non empty set
bool X is non empty set
l1 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l2 is Element of I
l1 . l2 is Element of X
i1 is Element of bool I
l1 .: i1 is Element of bool X
i2 is Element of bool X
(l1 .: i1) \ i2 is Element of bool X
l1 " i2 is Element of bool I
i1 \ (l1 " i2) is Element of bool I
I is non empty set
X is non empty set
[:I,X:] is non empty Relation-like set
bool [:I,X:] is non empty set
bool I is non empty set
bool X is non empty set
l1 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l1 " is Relation-like Function-like set
l2 is Element of X
(l1 ") . l2 is set
i1 is Element of bool I
l1 .: i1 is Element of bool X
i2 is Element of bool X
(l1 .: i1) \ i2 is Element of bool X
l1 " i2 is Element of bool I
i1 \ (l1 " i2) is Element of bool I
rng l1 is non empty Element of bool X
dom l1 is non empty Element of bool I
B is Element of I
l1 . B is Element of X
I is Relation-like Function-like set
proj1 I is set
X is set
{X} is non empty trivial 1 -element set
I | {X} is Relation-like Function-like set
I . X is set
X .--> (I . X) is trivial Relation-like {X} -defined Function-like one-to-one constant set
{X} --> (I . X) is non empty Relation-like {X} -defined {(I . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(I . X)}:]
{(I . X)} is non empty trivial 1 -element set
[:{X},{(I . X)}:] is non empty Relation-like set
bool [:{X},{(I . X)}:] is non empty set
[X,(I . X)] is V25() set
{X,(I . X)} is non empty set
{{X,(I . X)},{X}} is non empty set
{[X,(I . X)]} is non empty trivial Relation-like Function-like constant 1 -element set
I is set
X is set
I .--> X is trivial Relation-like {I} -defined Function-like one-to-one constant set
{I} is non empty trivial 1 -element set
{I} --> X is non empty Relation-like {I} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{I},{X}:]
{X} is non empty trivial 1 -element set
[:{I},{X}:] is non empty Relation-like set
bool [:{I},{X}:] is non empty set
I is set
X is set
l1 is set
l2 is set
(I,X) --> (l1,l2) is Relation-like Function-like set
I .--> l1 is non empty trivial Relation-like {I} -defined Function-like one-to-one constant 1 -element set
{I} is non empty trivial 1 -element set
{I} --> l1 is non empty Relation-like {I} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{I},{l1}:]
{l1} is non empty trivial 1 -element set
[:{I},{l1}:] is non empty Relation-like set
bool [:{I},{l1}:] is non empty set
X .--> l2 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l2 is non empty Relation-like {X} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{X},{l2}:]
{l2} is non empty trivial 1 -element set
[:{X},{l2}:] is non empty Relation-like set
bool [:{X},{l2}:] is non empty set
(I .--> l1) +* (X .--> l2) is non empty Relation-like Function-like set
I is set
X is Relation-like I -defined Function-like total set
l1 is set
X . l1 is set
l1 .--> (X . l1) is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> (X . l1) is non empty Relation-like {l1} -defined {(X . l1)} -valued Function-like constant total quasi_total Element of bool [:{l1},{(X . l1)}:]
{(X . l1)} is non empty trivial 1 -element set
[:{l1},{(X . l1)}:] is non empty Relation-like set
bool [:{l1},{(X . l1)}:] is non empty set
X | {l1} is Relation-like {l1} -defined I -defined Function-like set
dom X is Element of bool I
bool I is non empty set
I is set
X is set
[:I,X:] is Relation-like set
l1 is Relation-like [:I,X:] -defined Function-like total set
l2 is set
i1 is set
l1 . (l2,i1) is set
[l2,i1] is V25() set
{l2,i1} is non empty set
{l2} is non empty trivial 1 -element set
{{l2,i1},{l2}} is non empty set
l1 . [l2,i1] is set
(l2,i1) :-> (l1 . (l2,i1)) is non empty Relation-like [:{l2},{i1}:] -defined {(l1 . (l2,i1))} -valued Function-like total quasi_total Element of bool [:[:{l2},{i1}:],{(l1 . (l2,i1))}:]
{i1} is non empty trivial 1 -element set
[:{l2},{i1}:] is non empty Relation-like set
{(l1 . (l2,i1))} is non empty trivial 1 -element set
[:[:{l2},{i1}:],{(l1 . (l2,i1))}:] is non empty Relation-like set
bool [:[:{l2},{i1}:],{(l1 . (l2,i1))}:] is non empty set
{[l2,i1]} is non empty trivial Relation-like Function-like constant 1 -element set
{[l2,i1]} --> (l1 . (l2,i1)) is non empty Relation-like {[l2,i1]} -defined {(l1 . (l2,i1))} -valued Function-like constant total quasi_total Element of bool [:{[l2,i1]},{(l1 . (l2,i1))}:]
[:{[l2,i1]},{(l1 . (l2,i1))}:] is non empty Relation-like set
bool [:{[l2,i1]},{(l1 . (l2,i1))}:] is non empty set
l1 | [:{l2},{i1}:] is Relation-like [:{l2},{i1}:] -defined [:I,X:] -defined Function-like set
[l2,i1] .--> (l1 . [l2,i1]) is non empty trivial Relation-like {[l2,i1]} -defined Function-like one-to-one constant 1 -element set
{[l2,i1]} --> (l1 . [l2,i1]) is non empty Relation-like {[l2,i1]} -defined {(l1 . [l2,i1])} -valued Function-like constant total quasi_total Element of bool [:{[l2,i1]},{(l1 . [l2,i1])}:]
{(l1 . [l2,i1])} is non empty trivial 1 -element set
[:{[l2,i1]},{(l1 . [l2,i1])}:] is non empty Relation-like set
bool [:{[l2,i1]},{(l1 . [l2,i1])}:] is non empty set
l1 | {[l2,i1]} is Relation-like {[l2,i1]} -defined [:I,X:] -defined Function-like set
l1 is Relation-like Function-like set
proj2 l1 is set
I is Relation-like Function-like set
proj1 I is set
X is Relation-like Function-like set
X +* l1 is Relation-like Function-like set
(X +* l1) (#) I is Relation-like Function-like set
X (#) I is Relation-like Function-like set
l1 (#) I is Relation-like Function-like set
(X (#) I) +* (l1 (#) I) is Relation-like Function-like set
proj1 l1 is set
proj1 (X +* l1) is set
proj1 X is set
proj1 ((X +* l1) (#) I) is set
proj1 (X (#) I) is set
proj1 (l1 (#) I) is set
(proj1 (X (#) I)) \/ (proj1 (l1 (#) I)) is set
l2 is set
(X +* l1) . l2 is set
(proj1 X) \/ (proj1 l1) is set
l1 . l2 is set
X . l2 is set
l2 is set
l1 . l2 is set
(X +* l1) . l2 is set
l1 . l2 is set
(X +* l1) . l2 is set
X . l2 is set
l2 is set
((X +* l1) (#) I) . l2 is set
(l1 (#) I) . l2 is set
(X +* l1) . l2 is set
I . ((X +* l1) . l2) is set
l1 . l2 is set
I . (l1 . l2) is set
l1 . l2 is set
(X +* l1) . l2 is set
I . ((X +* l1) . l2) is set
X . l2 is set
I . (X . l2) is set
(X (#) I) . l2 is set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
X +* l1 is Relation-like Function-like set
I (#) (X +* l1) is Relation-like Function-like set
I (#) X is Relation-like Function-like set
I (#) l1 is Relation-like Function-like set
(I (#) X) +* (I (#) l1) is Relation-like Function-like set
proj1 (I (#) (X +* l1)) is set
proj1 (I (#) X) is set
proj1 (I (#) l1) is set
(proj1 (I (#) X)) \/ (proj1 (I (#) l1)) is set
l2 is set
I . l2 is set
proj1 (X +* l1) is set
proj1 X is set
proj1 l1 is set
(proj1 X) \/ (proj1 l1) is set
proj1 I is set
l2 is set
I . l2 is set
proj1 X is set
proj1 l1 is set
(proj1 X) \/ (proj1 l1) is set
proj1 (X +* l1) is set
proj1 I is set
l2 is set
proj1 I is set
I . l2 is set
proj1 l1 is set
(I (#) (X +* l1)) . l2 is set
(X +* l1) . (I . l2) is set
l1 . (I . l2) is set
(I (#) l1) . l2 is set
X . (I . l2) is set
(I (#) X) . l2 is set
I is Relation-like Function-like set
proj2 I is set
X is Relation-like Function-like set
proj1 X is set
l1 is Relation-like Function-like set
l1 +* X is Relation-like Function-like set
I (#) (l1 +* X) is Relation-like Function-like set
I (#) l1 is Relation-like Function-like set
I (#) X is Relation-like Function-like set
(I (#) l1) +* (I (#) X) is Relation-like Function-like set
(I (#) l1) +* {} is Relation-like Function-like set
I is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
l1 is set
I --> l1 is Relation-like I -defined {l1} -valued Function-like constant total quasi_total Element of bool [:I,{l1}:]
{l1} is non empty trivial 1 -element set
[:I,{l1}:] is Relation-like set
bool [:I,{l1}:] is non empty set
(id X) +* (I --> l1) is Relation-like Function-like set
proj2 ((id X) +* (I --> l1)) is set
l2 is set
proj1 ((id X) +* (I --> l1)) is set
i1 is set
((id X) +* (I --> l1)) . i1 is set
dom (id X) is Element of bool X
bool X is non empty set
dom (I --> l1) is Element of bool I
bool I is non empty set
(dom (id X)) \/ (dom (I --> l1)) is set
(I --> l1) . i1 is set
(id X) . i1 is set
I is set
X is set
I .--> X is non empty trivial Relation-like {I} -defined Function-like one-to-one constant 1 -element set
{I} is non empty trivial 1 -element set
{I} --> X is non empty Relation-like {I} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{I},{X}:]
{X} is non empty trivial 1 -element set
[:{I},{X}:] is non empty Relation-like set
bool [:{I},{X}:] is non empty set
l1 is set
id l1 is Relation-like l1 -defined l1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:l1,l1:]
[:l1,l1:] is Relation-like set
bool [:l1,l1:] is non empty set
(id l1) +* (I .--> X) is non empty Relation-like Function-like set
proj2 ((id l1) +* (I .--> X)) is non empty set
(id l1) +* ({I} --> X) is non empty Relation-like Function-like set
proj2 ((id l1) +* ({I} --> X)) is non empty set
I is set
X is set
{X} is non empty trivial 1 -element set
I \/ {X} is non empty set
l1 is Relation-like Function-like set
proj1 l1 is set
l1 | I is Relation-like Function-like set
l1 . X is set
X .--> (l1 . X) is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} --> (l1 . X) is non empty Relation-like {X} -defined {(l1 . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(l1 . X)}:]
{(l1 . X)} is non empty trivial 1 -element set
[:{X},{(l1 . X)}:] is non empty Relation-like set
bool [:{X},{(l1 . X)}:] is non empty set
(l1 | I) +* (X .--> (l1 . X)) is non empty Relation-like Function-like set
l1 | {X} is Relation-like Function-like set
(l1 | I) +* (l1 | {X}) is Relation-like Function-like set
I is Relation-like Function-like set
X is set
l1 is set
X --> l1 is Relation-like X -defined {l1} -valued Function-like constant total quasi_total Element of bool [:X,{l1}:]
{l1} is non empty trivial 1 -element set
[:X,{l1}:] is Relation-like set
bool [:X,{l1}:] is non empty set
I +* (X --> l1) is Relation-like Function-like set
l2 is set
X --> l2 is Relation-like X -defined {l2} -valued Function-like constant total quasi_total Element of bool [:X,{l2}:]
{l2} is non empty trivial 1 -element set
[:X,{l2}:] is Relation-like set
bool [:X,{l2}:] is non empty set
(I +* (X --> l1)) +* (X --> l2) is Relation-like Function-like set
I +* (X --> l2) is Relation-like Function-like set
dom (X --> l2) is Element of bool X
bool X is non empty set
dom (X --> l1) is Element of bool X
proj1 (I +* (X --> l1)) is set
proj1 I is set
(proj1 I) \/ X is set
proj1 ((I +* (X --> l1)) +* (X --> l2)) is set
((proj1 I) \/ X) \/ X is set
X \/ X is set
(proj1 I) \/ (X \/ X) is set
i1 is set
((I +* (X --> l1)) +* (X --> l2)) . i1 is set
(X --> l2) . i1 is set
(I +* (X --> l2)) . i1 is set
((I +* (X --> l1)) +* (X --> l2)) . i1 is set
(I +* (X --> l1)) . i1 is set
I . i1 is set
(I +* (X --> l2)) . i1 is set
proj1 (I +* (X --> l2)) is set
INT * is non empty functional FinSequence-membered FinSequenceSet of INT
I is set
X is set
[I,X] is V25() set
{I,X} is non empty set
{I} is non empty trivial 1 -element set
{{I,X},{I}} is non empty set
{} * is non empty functional FinSequence-membered FinSequenceSet of {}
I is set
X is empty Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional non total V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of {}
dom X is empty proper Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V92() Element of bool NAT
l1 is set
I is set
I is set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X is set
X * is non empty functional FinSequence-membered FinSequenceSet of X
proj2 <*I*> is non empty trivial 1 -element set
{I} is non empty trivial 1 -element set
I is set
I * is non empty functional FinSequence-membered FinSequenceSet of I
X is set
X * is non empty functional FinSequence-membered FinSequenceSet of X
l1 is set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
I is Element of bool NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
{ b₁ where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : not l1 + 1 <= b₁ } is set
l2 is set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
I is finite set
bool I is non empty set
bool (bool I) is non empty set
X is non empty Element of bool (bool I)
COMPLEMENT X is Element of bool (bool I)
l1 is non empty Element of bool (bool I)
l2 is set
i1 is Element of bool I
i1 ` is Element of bool I
i2 is Element of X
B is Element of X
B ` is Element of bool I
(B `) ` is Element of bool I
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom X is V92() Element of bool NAT
dom I is V92() Element of bool NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*0*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*<*0*>*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
I is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
dom I is non empty trivial 1 -element V92() Element of bool NAT
{1} is non empty trivial 1 -element Element of bool NAT
I . 1 is set
<*0*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
X is set
proj1 I is non empty trivial 1 -element V92() set
I . X is set
X is set
proj1 I is non empty trivial 1 -element V92() set
I . X is set
I is Relation-like Function-like set
I is Relation-like Function-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X is set
proj1 <*I*> is non empty trivial 1 -element V92() set
<*I*> . X is set
dom <*I*> is non empty trivial 1 -element V92() Element of bool NAT
{1} is non empty trivial 1 -element Element of bool NAT
X is Relation-like Function-like set
<*I,X*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
l1 is set
proj1 <*I,X*> is non empty 2 -element V92() set
<*I,X*> . l1 is set
dom <*I,X*> is non empty 2 -element V92() Element of bool NAT
{1,2} is non empty Element of bool NAT
l1 is Relation-like Function-like set
<*I,X,l1*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set
l2 is set
proj1 <*I,X,l1*> is non empty 3 -element V92() set
<*I,X,l1*> . l2 is set
dom <*I,X,l1*> is non empty 3 -element V92() Element of bool NAT
{1,2,3} is non empty Element of bool NAT
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like Function-like set
I |-> X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg I is finite I -element Element of bool NAT
(Seg I) --> X is Relation-like Seg I -defined {X} -valued Function-like constant total quasi_total Function-yielding V41() Element of bool [:(Seg I),{X}:]
{X} is non empty trivial functional 1 -element set
[:(Seg I),{X}:] is Relation-like set
bool [:(Seg I),{X}:] is non empty set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
I ^ X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l1 is set
proj1 (I ^ X) is V92() set
(I ^ X) . l1 is set
dom (I ^ X) is V92() Element of bool NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
I . l2 is Relation-like Function-like set
(I ^ X) . l2 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
dom X is V92() Element of bool NAT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(len I) + i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X . i1 is Relation-like Function-like set
(I ^ X) . l2 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I ^ X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (I ^ X) is V92() Element of bool NAT
l1 is set
dom I is V92() Element of bool NAT
(I ^ X) . l1 is set
I . l1 is set
l1 is set
proj1 X is V92() set
X . l1 is set
dom X is V92() Element of bool NAT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I ^ X) . ((len I) + l2) is set
F₁() is non empty set
F₂() is non empty set
F₃() is non empty set
[:F₁(),F₂():] is non empty Relation-like set
[:[:F₁(),F₂():],F₃():] is non empty Relation-like set
bool [:[:F₁(),F₂():],F₃():] is non empty set
I is Element of [:F₁(),F₂():]
I `1 is Element of F<sub>1</sub>()
I `2 is Element of F₂()
F₄((I `1),(I `2)) is set
I is non empty Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like total quasi_total Element of bool [:[:F₁(),F₂():],F₃():]
X is Element of F₁()
l1 is Element of F₂()
I . (X,l1) is Element of F₃()
[X,l1] is V25() set
{X,l1} is non empty set
{X} is non empty trivial 1 -element set
{{X,l1},{X}} is non empty set
I . [X,l1] is set
F₄(X,l1) is set
[X,l1] is V25() Element of [:F₁(),F₂():]
[X,l1] `1 is Element of F<sub>1</sub>()
[X,l1] `2 is Element of F₂()
F₁() is set
F₂() is non empty set
{ F₃(b₁) where b₁ is Element of F₂() : F₄(b₁) in F₁() } is set
the Element of { F₃(b₁) where b₁ is Element of F₂() : F₄(b₁) in F₁() } is Element of { F₃(b₁) where b₁ is Element of F₂() : F₄(b₁) in F₁() }
X is Element of F₂()
F₃(X) is set
F₄(X) is set
I is non empty set
{ b₁ where b₁ is Element of F₂() : F₄(b₁) in I } is set
{ b₁ where b₁ is Element of I : S₁[b₁] } is set
{ F₃(b₁) where b₁ is Element of F₂() : b₁ in { b₁ where b₂ is Element of F₂() : F₄(b₁) in I } } is set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
F₄(i1) is set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
i2 is Element of F₂()
F₄(i2) is set
{ [F₄(b₁),b₁] where b₁ is Element of F₂() : verum } is set
l2 is set
i1 is set
i2 is Element of I
B is Element of F₂()
F₄(B) is set
B is Element of F₂()
F₄(B) is set
B is set
e is set
[i1,e] is V25() set
{i1,e} is non empty set
{i1} is non empty trivial 1 -element set
{{i1,e},{i1}} is non empty set
i1 is set
i2 is Element of F₂()
F₄(i2) is set
B is set
B is set
[B,i1] is V25() set
{B,i1} is non empty set
{B} is non empty trivial 1 -element set
{{B,i1},{B}} is non empty set
i1 is set
i2 is set
[i1,i2] is V25() set
{i1,i2} is non empty set
{i1} is non empty trivial 1 -element set
{{i1,i2},{i1}} is non empty set
B is set
B is set
[B,B] is V25() set
{B,B} is non empty set
{B} is non empty trivial 1 -element set
{{B,B},{B}} is non empty set
e is Element of F₂()
F₄(e) is set
[F₄(e),e] is V25() set
{F₄(e),e} is non empty set
{F₄(e)} is non empty trivial 1 -element set
{{F₄(e),e},{F₄(e)}} is non empty set
l is Element of F₂()
F₄(l) is set
[F₄(l),l] is V25() set
{F₄(l),l} is non empty set
{F₄(l)} is non empty trivial 1 -element set
{{F₄(l),l},{F₄(l)}} is non empty set
bool I is non empty set
F₁() is set
F₂() is non empty set
{ b₁ where b₁ is Element of F₂() : F₃(b₁) in F₁() } is set
the Element of { b₁ where b₁ is Element of F₂() : F₃(b₁) in F₁() } is Element of { b₁ where b₁ is Element of F₂() : F₃(b₁) in F₁() }
l1 is Element of F₂()
F₃(l1) is set
X is non empty set
{ [F₃(b₁),b₁] where b₁ is Element of F₂() : verum } is set
l1 is set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
i2 is set
B is set
[l2,B] is V25() set
{l2,B} is non empty set
{l2} is non empty trivial 1 -element set
{{l2,B},{l2}} is non empty set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
i2 is set
B is set
[B,l2] is V25() set
{B,l2} is non empty set
{B} is non empty trivial 1 -element set
{{B,l2},{B}} is non empty set
l2 is set
i1 is set
[l2,i1] is V25() set
{l2,i1} is non empty set
{l2} is non empty trivial 1 -element set
{{l2,i1},{l2}} is non empty set
i2 is set
B is set
[i2,B] is V25() set
{i2,B} is non empty set
{i2} is non empty trivial 1 -element set
{{i2,B},{i2}} is non empty set
B is Element of F₂()
F₃(B) is set
[F₃(B),B] is V25() set
{F₃(B),B} is non empty set
{F₃(B)} is non empty trivial 1 -element set
{{F₃(B),B},{F₃(B)}} is non empty set
e is Element of F₂()
F₃(e) is set
[F₃(e),e] is V25() set
{F₃(e),e} is non empty set
{F₃(e)} is non empty trivial 1 -element set
{{F₃(e),e},{F₃(e)}} is non empty set
F₁() is set
F₂() is non empty set
{ F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() } is set
the Element of { F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() } is Element of { F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() }
X is Element of F₂()
F₃(X) is set
I is non empty set
{ F₃(b₁) where b₁ is Element of F₂() : b₁ in I } is set
{ [b₁,F₃(b₁)] where b₁ is Element of F₂() : verum } is set
l1 is set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
i2 is set
[l2,i2] is V25() set
{l2,i2} is non empty set
{l2} is non empty trivial 1 -element set
{{l2,i2},{l2}} is non empty set
l2 is set
i1 is Element of F₂()
F₃(i1) is set
i2 is set
B is set
[B,l2] is V25() set
{B,l2} is non empty set
{B} is non empty trivial 1 -element set
{{B,l2},{B}} is non empty set
l2 is set
i1 is set
[l2,i1] is V25() set
{l2,i1} is non empty set
{l2} is non empty trivial 1 -element set
{{l2,i1},{l2}} is non empty set
i2 is set
B is set
[i2,B] is V25() set
{i2,B} is non empty set
{i2} is non empty trivial 1 -element set
{{i2,B},{i2}} is non empty set
B is Element of F₂()
F₃(B) is set
[B,F₃(B)] is V25() set
{B,F₃(B)} is non empty set
{B} is non empty trivial 1 -element set
{{B,F₃(B)},{B}} is non empty set
e is Element of F₂()
F₃(e) is set
[e,F₃(e)] is V25() set
{e,F₃(e)} is non empty set
{e} is non empty trivial 1 -element set
{{e,F₃(e)},{e}} is non empty set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
I ^ <*X*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*X*> . 1 is set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
I is set
X is set
I is set
X is set
(I,X) is Element of X
l1 is set
X /\ l1 is set
(I,l1) is Element of l1
I is Relation-like Function-like set
X is set
proj1 I is set
(proj1 I) \ X is Element of bool (proj1 I)
bool (proj1 I) is non empty set
I | ((proj1 I) \ X) is Relation-like Function-like set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is set
proj1 I is set
(proj1 I) \ l1 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
I | ((proj1 I) \ l1) is Relation-like Function-like set
proj1 X is set
(proj1 X) \ l1 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
X | ((proj1 X) \ l1) is Relation-like Function-like set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
l2 is set
proj1 I is set
(proj1 I) \ l2 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
I | ((proj1 I) \ l2) is Relation-like Function-like set
proj1 X is set
(proj1 X) \ l2 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
X | ((proj1 X) \ l2) is Relation-like Function-like set
proj1 l1 is set
(proj1 l1) \ l2 is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
l1 | ((proj1 l1) \ l2) is Relation-like Function-like set
I is Relation-like Function-like set
X is Relation-like Function-like set
proj1 I is set
proj1 X is set
l1 is set
(proj1 I) \ l1 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
(proj1 X) \ l1 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
I | ((proj1 I) \ l1) is Relation-like Function-like set
X | ((proj1 X) \ l1) is Relation-like Function-like set
(proj1 I) /\ ((proj1 I) \ l1) is Element of bool (proj1 I)
proj1 (I | ((proj1 I) \ l1)) is set
(proj1 X) /\ ((proj1 X) \ l1) is Element of bool (proj1 X)
X is Relation-like Function-like set
proj1 X is set
I is Relation-like Function-like set
I +* X is Relation-like Function-like set
l1 is set
proj1 (I +* X) is set
(proj1 (I +* X)) \ l1 is Element of bool (proj1 (I +* X))
bool (proj1 (I +* X)) is non empty set
proj1 I is set
(proj1 I) \/ (proj1 X) is set
((proj1 I) \/ (proj1 X)) \ l1 is Element of bool ((proj1 I) \/ (proj1 X))
bool ((proj1 I) \/ (proj1 X)) is non empty set
(proj1 I) \ l1 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
(proj1 X) \ l1 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
((proj1 I) \ l1) \/ ((proj1 X) \ l1) is set
((proj1 I) \ l1) \/ {} is set
I | ((proj1 I) \ l1) is Relation-like Function-like set
(I +* X) | ((proj1 (I +* X)) \ l1) is Relation-like Function-like set
X is set
I is Relation-like Function-like set
proj1 I is set
l1 is set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
I is Relation-like Function-like set
proj1 I is set
l1 is set
X is set
(I,l1,X) is Relation-like Function-like set
proj1 (I,l1,X) is set
{l1} is non empty trivial 1 -element set
l1 .--> X is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} --> X is non empty Relation-like {l1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{l1},{X}:]
{X} is non empty trivial 1 -element set
[:{l1},{X}:] is non empty Relation-like set
bool [:{l1},{X}:] is non empty set
I +* (l1 .--> X) is non empty Relation-like Function-like set
proj1 (I +* (l1 .--> X)) is non empty set
dom (l1 .--> X) is non empty trivial 1 -element Element of bool {l1}
bool {l1} is non empty set
(proj1 I) \/ (dom (l1 .--> X)) is non empty set
(proj1 I) \/ {l1} is non empty set
I is Relation-like Function-like set
proj1 I is set
l1 is set
X is set
(I,l1,X) is Relation-like Function-like set
(I,l1,X) . l1 is set
{l1} is non empty trivial 1 -element set
l1 .--> X is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} --> X is non empty Relation-like {l1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{l1},{X}:]
{X} is non empty trivial 1 -element set
[:{l1},{X}:] is non empty Relation-like set
bool [:{l1},{X}:] is non empty set
dom (l1 .--> X) is non empty trivial 1 -element Element of bool {l1}
bool {l1} is non empty set
I +* (l1 .--> X) is non empty Relation-like Function-like set
(I +* (l1 .--> X)) . l1 is set
(l1 .--> X) . l1 is set
I is Relation-like Function-like set
l1 is set
l2 is set
X is set
(I,l1,X) is Relation-like Function-like set
(I,l1,X) . l2 is set
I . l2 is set
{l1} is non empty trivial 1 -element set
l1 .--> X is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} --> X is non empty Relation-like {l1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{l1},{X}:]
{X} is non empty trivial 1 -element set
[:{l1},{X}:] is non empty Relation-like set
bool [:{l1},{X}:] is non empty set
dom (l1 .--> X) is non empty trivial 1 -element Element of bool {l1}
bool {l1} is non empty set
proj1 I is set
I +* (l1 .--> X) is non empty Relation-like Function-like set
(I +* (l1 .--> X)) . l2 is set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
l2 is set
i1 is set
X is set
(I,l2,X) is Relation-like Function-like set
l1 is set
((I,l2,X),i1,l1) is Relation-like Function-like set
(I,i1,l1) is Relation-like Function-like set
((I,i1,l1),l2,X) is Relation-like Function-like set
proj1 I is set
proj1 (I,i1,l1) is set
{l2} is non empty trivial 1 -element set
l2 .--> X is non empty trivial Relation-like {l2} -defined Function-like one-to-one constant 1 -element set
{l2} --> X is non empty Relation-like {l2} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{l2},{X}:]
{X} is non empty trivial 1 -element set
[:{l2},{X}:] is non empty Relation-like set
bool [:{l2},{X}:] is non empty set
dom (l2 .--> X) is non empty trivial 1 -element Element of bool {l2}
bool {l2} is non empty set
{i1} is non empty trivial 1 -element set
i1 .--> l1 is non empty trivial Relation-like {i1} -defined Function-like one-to-one constant 1 -element set
{i1} --> l1 is non empty Relation-like {i1} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{i1},{l1}:]
{l1} is non empty trivial 1 -element set
[:{i1},{l1}:] is non empty Relation-like set
bool [:{i1},{l1}:] is non empty set
dom (i1 .--> l1) is non empty trivial 1 -element Element of bool {i1}
bool {i1} is non empty set
proj1 (I,l2,X) is set
(I,l2,X) +* (i1 .--> l1) is non empty Relation-like Function-like set
I +* (l2 .--> X) is non empty Relation-like Function-like set
(I +* (l2 .--> X)) +* (i1 .--> l1) is non empty Relation-like Function-like set
(l2 .--> X) +* (i1 .--> l1) is non empty Relation-like Function-like set
I +* ((l2 .--> X) +* (i1 .--> l1)) is non empty Relation-like Function-like set
(i1 .--> l1) +* (l2 .--> X) is non empty Relation-like Function-like set
I +* ((i1 .--> l1) +* (l2 .--> X)) is non empty Relation-like Function-like set
I +* (i1 .--> l1) is non empty Relation-like Function-like set
(I +* (i1 .--> l1)) +* (l2 .--> X) is non empty Relation-like Function-like set
(I,i1,l1) +* (l2 .--> X) is non empty Relation-like Function-like set
proj1 I is set
proj1 (I,l2,X) is set
proj1 I is set
proj1 (I,i1,l1) is set
proj1 I is set
proj1 (I,i1,l1) is set
proj1 (I,l2,X) is set
proj1 I is set
I is Relation-like Function-like set
l2 is set
X is set
(I,l2,X) is Relation-like Function-like set
l1 is set
((I,l2,X),l2,l1) is Relation-like Function-like set
(I,l2,l1) is Relation-like Function-like set
{l2} is non empty trivial 1 -element set
l2 .--> X is non empty trivial Relation-like {l2} -defined Function-like one-to-one constant 1 -element set
{l2} --> X is non empty Relation-like {l2} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{l2},{X}:]
{X} is non empty trivial 1 -element set
[:{l2},{X}:] is non empty Relation-like set
bool [:{l2},{X}:] is non empty set
dom (l2 .--> X) is non empty trivial 1 -element Element of bool {l2}
bool {l2} is non empty set
l2 .--> l1 is non empty trivial Relation-like {l2} -defined Function-like one-to-one constant 1 -element set
{l2} --> l1 is non empty Relation-like {l2} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{l2},{l1}:]
{l1} is non empty trivial 1 -element set
[:{l2},{l1}:] is non empty Relation-like set
bool [:{l2},{l1}:] is non empty set
dom (l2 .--> l1) is non empty trivial 1 -element Element of bool {l2}
proj1 I is set
proj1 (I,l2,X) is set
(I,l2,X) +* (l2 .--> l1) is non empty Relation-like Function-like set
I +* (l2 .--> X) is non empty Relation-like Function-like set
(I +* (l2 .--> X)) +* (l2 .--> l1) is non empty Relation-like Function-like set
(l2 .--> X) +* (l2 .--> l1) is non empty Relation-like {l2} -defined Function-like set
I +* ((l2 .--> X) +* (l2 .--> l1)) is non empty Relation-like Function-like set
I +* (l2 .--> l1) is non empty Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
X is set
I . X is set
(I,X,(I . X)) is Relation-like Function-like set
proj1 I is set
X .--> (I . X) is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> (I . X) is non empty Relation-like {X} -defined {(I . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(I . X)}:]
{(I . X)} is non empty trivial 1 -element set
[:{X},{(I . X)}:] is non empty Relation-like set
bool [:{X},{(I . X)}:] is non empty set
I | {X} is Relation-like Function-like set
I +* (X .--> (I . X)) is non empty Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj1 (I,X,l1) is set
dom I is V92() Element of bool NAT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
Seg (len I) is finite len I -element Element of bool NAT
I is set
X is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Element of I
(X,l1,l2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom X is V92() Element of bool NAT
X . l1 is set
rng X is Element of bool I
bool I is non empty set
{l2} is non empty trivial 1 -element set
l1 .--> l2 is non empty trivial Relation-like NAT -defined {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
proj2 (l1 .--> l2) is non empty trivial 1 -element set
(rng X) \/ (proj2 (l1 .--> l2)) is non empty set
(rng X) \/ {l2} is non empty set
X +* (l1 .--> l2) is non empty Relation-like NAT -defined Function-like set
proj2 (X,l1,l2) is set
dom X is V92() Element of bool NAT
dom X is V92() Element of bool NAT
I is non empty set
X is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
dom X is V92() Element of bool NAT
l1 is Element of I
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I,X,l2,l1) is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
(I,X,l2,l1) /. l2 is Element of I
dom (I,X,l2,l1) is V92() Element of bool NAT
(I,X,l2,l1) . l2 is set
I is non empty set
X is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
dom X is V92() Element of bool NAT
l1 is Element of I
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I,X,l2,l1) is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
(I,X,l2,l1) /. i1 is Element of I
X /. i1 is Element of I
dom (I,X,l2,l1) is V92() Element of bool NAT
(I,X,l2,l1) . i1 is set
X . i1 is set
I is non empty set
X is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X /. i1 is Element of I
(I,X,i1,(X /. i1)) is Relation-like NAT -defined I -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of I
dom X is V92() Element of bool NAT
X . i1 is set
(X,i1,(X . i1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom X is V92() Element of bool NAT
dom X is V92() Element of bool NAT
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
dom X is V92() Element of bool NAT
l1 is Relation-like Function-like set
l2 is Relation-like Function-like set
i1 is Relation-like NAT -defined Function-like total Function-yielding V41() set
i1 . (len X) is Relation-like Function-like set
i1 . 0 is Relation-like Function-like set
i2 is Relation-like NAT -defined Function-like total Function-yielding V41() set
i2 . (len X) is Relation-like Function-like set
i2 . 0 is Relation-like Function-like set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 . B is Relation-like Function-like set
i2 . B is Relation-like Function-like set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i1 . (B + 1) is Relation-like Function-like set
i2 . (B + 1) is Relation-like Function-like set
X . (B + 1) is Relation-like Function-like set
e is Relation-like Function-like set
B is Relation-like Function-like set
e (#) B is Relation-like Function-like set
l1 is Relation-like Function-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X . (l2 + 1) is Relation-like Function-like set
i1 is set
B is Relation-like Function-like set
i2 is Relation-like Function-like set
B (#) i2 is Relation-like Function-like set
B is Relation-like Function-like set
e is Relation-like Function-like set
B (#) e is Relation-like Function-like set
B is Relation-like Function-like set
B is Relation-like Function-like set
B (#) B is Relation-like Function-like set
l2 is Relation-like Function-like set
proj1 l2 is set
l2 . 0 is set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 . i1 is set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l2 . (i1 + 1) is set
X . (i1 + 1) is Relation-like Function-like set
B is Relation-like Function-like set
i2 is Relation-like Function-like set
B (#) i2 is Relation-like Function-like set
l2 . (len X) is set
i2 is set
l2 . i2 is set
i1 is Relation-like Function-like set
i2 is Relation-like NAT -defined Function-like total Function-yielding V41() set
i2 . (len X) is Relation-like Function-like set
i2 . 0 is Relation-like Function-like set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . B is Relation-like Function-like set
X . (B + 1) is Relation-like Function-like set
i2 . (B + 1) is Relation-like Function-like set
B is Relation-like Function-like set
e is Relation-like Function-like set
B (#) e is Relation-like Function-like set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X is set
dom I is V92() Element of bool NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . l1 is Relation-like Function-like set
i1 is set
l2 is Relation-like Function-like set
l2 . i1 is set
l1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 . 1 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . l2 is Relation-like Function-like set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (l2 + 1) is set
l1 . l2 is set
i1 is Relation-like Function-like set
i1 . (l1 . l2) is set
i2 is Relation-like Function-like set
i2 . (l1 . l2) is set
l1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 . 1 is set
l2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 . 1 is set
dom l1 is V92() Element of bool NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 . i1 is set
l2 . i1 is set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (i1 + 1) is set
l2 . (i1 + 1) is set
I . i1 is Relation-like Function-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 is Relation-like Function-like set
i2 . (l2 . i1) is set
l1 . 0 is set
l2 . 0 is set
dom l2 is V92() Element of bool NAT
I is set
(I,{}) is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
dom {} is empty proper Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V92() Element of bool NAT
X is Relation-like NAT -defined Function-like total Function-yielding V41() set
X . 0 is Relation-like Function-like set
I is set
({},I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len ({},I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
({},I) . 1 is set
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,X) is Relation-like Function-like set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
X ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(X ^ <*l1*>)) is Relation-like Function-like set
(I,X) (#) l1 is Relation-like Function-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X ^ <*l1*>) . ((len X) + 1) is Relation-like Function-like set
len <*l1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (X ^ <*l1*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
dom (X ^ <*l1*>) is non empty V92() Element of bool NAT
l2 is Relation-like NAT -defined Function-like total Function-yielding V41() set
l2 . (len (X ^ <*l1*>)) is Relation-like Function-like set
l2 . 0 is Relation-like Function-like set
l2 . (len X) is Relation-like Function-like set
dom X is V92() Element of bool NAT
i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
B is Relation-like Function-like set
l2 . i2 is Relation-like Function-like set
B is Relation-like Function-like set
X . (i2 + 1) is Relation-like Function-like set
(X ^ <*l1*>) . (i2 + 1) is Relation-like Function-like set
l2 . (i2 + 1) is Relation-like Function-like set
B (#) B is Relation-like Function-like set
i1 is Relation-like Function-like set
dom <*l1*> is non empty trivial 1 -element V92() Element of bool NAT
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(X,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,I) . ((len X) + 1) is set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
X ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ <*l1*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l1 . ((X,I) . ((len X) + 1)) is set
<*(l1 . ((X,I) . ((len X) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(X,I) ^ <*(l1 . ((X,I) . ((len X) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (X,I) is V92() Element of bool NAT
len (X,I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(X,I) . 1 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
((X ^ <*l1*>),I) . l2 is set
(X,I) . l2 is set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ <*l1*>),I) . (l2 + 1) is set
(X,I) . (l2 + 1) is set
X . l2 is Relation-like Function-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom X is V92() Element of bool NAT
dom (X ^ <*l1*>) is non empty V92() Element of bool NAT
i1 is Relation-like Function-like set
(X ^ <*l1*>) . l2 is Relation-like Function-like set
i1 . (((X ^ <*l1*>),I) . l2) is set
((X ^ <*l1*>),I) . 0 is set
(X,I) . 0 is set
len <*l1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (X ^ <*l1*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X ^ <*l1*>) . ((len X) + 1) is Relation-like Function-like set
dom (X ^ <*l1*>) is non empty V92() Element of bool NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
dom <*(l1 . ((X,I) . ((len X) + 1)))*> is non empty trivial 1 -element V92() Element of bool NAT
(len X) + l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ <*l1*>),I) . ((len X) + l2) is set
l1 . (((X ^ <*l1*>),I) . ((len X) + l2)) is set
(len (X,I)) + l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ <*l1*>),I) . ((len (X,I)) + l2) is set
(X,I) . ((len X) + l2) is set
<*(l1 . ((X,I) . ((len X) + 1)))*> . l2 is set
len ((X ^ <*l1*>),I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ <*l1*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len <*(l1 . ((X,I) . ((len X) + 1)))*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom ((X ^ <*l1*>),I) is V92() Element of bool NAT
(len (X,I)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
Seg ((len (X,I)) + 1) is non empty finite (len (X,I)) + 1 -element Element of bool NAT
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*l1*> ^ X is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(<*l1*> ^ X)) is Relation-like Function-like set
l1 | I is Relation-like Function-like set
l1 .: I is set
((l1 .: I),X) is Relation-like Function-like set
(l1 | I) (#) ((l1 .: I),X) is Relation-like Function-like set
l2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
<*l1*> ^ l2 is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(<*l1*> ^ l2)) is Relation-like Function-like set
((l1 .: I),l2) is Relation-like Function-like set
(l1 | I) (#) ((l1 .: I),l2) is Relation-like Function-like set
i1 is Relation-like Function-like set
<*i1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
l2 ^ <*i1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
<*l1*> ^ (l2 ^ <*i1*>) is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(<*l1*> ^ (l2 ^ <*i1*>))) is Relation-like Function-like set
((l1 .: I),(l2 ^ <*i1*>)) is Relation-like Function-like set
(l1 | I) (#) ((l1 .: I),(l2 ^ <*i1*>)) is Relation-like Function-like set
(<*l1*> ^ l2) ^ <*i1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,((<*l1*> ^ l2) ^ <*i1*>)) is Relation-like Function-like set
(I,(<*l1*> ^ l2)) (#) i1 is Relation-like Function-like set
((l1 .: I),l2) (#) i1 is Relation-like Function-like set
(l1 | I) (#) (((l1 .: I),l2) (#) i1) is Relation-like Function-like set
<*l1*> ^ {} is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
{} ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(<*l1*> ^ {})) is Relation-like Function-like set
(I,{}) is Relation-like Function-like set
(I,{}) (#) l1 is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
(id I) (#) l1 is Relation-like I -defined Function-like set
proj2 (l1 | I) is set
id (proj2 (l1 | I)) is Relation-like proj2 (l1 | I) -defined proj2 (l1 | I) -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj2 (l1 | I)),(proj2 (l1 | I)):]
[:(proj2 (l1 | I)),(proj2 (l1 | I)):] is Relation-like set
bool [:(proj2 (l1 | I)),(proj2 (l1 | I)):] is non empty set
(l1 | I) (#) (id (proj2 (l1 | I))) is Relation-like proj2 (l1 | I) -valued Function-like set
id (l1 .: I) is Relation-like l1 .: I -defined l1 .: I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(l1 .: I),(l1 .: I):]
[:(l1 .: I),(l1 .: I):] is Relation-like set
bool [:(l1 .: I),(l1 .: I):] is non empty set
(l1 | I) (#) (id (l1 .: I)) is Relation-like l1 .: I -valued Function-like set
((l1 .: I),{}) is Relation-like Function-like set
(l1 | I) (#) ((l1 .: I),{}) is Relation-like Function-like set
I is set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*l1*> ^ X is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((<*l1*> ^ X),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l1 . I is set
(X,(l1 . I)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ (X,(l1 . I)) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
l2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
<*l1*> ^ l2 is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((<*l1*> ^ l2),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(l2,(l1 . I)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ (l2,(l1 . I)) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i1 is Relation-like Function-like set
<*i1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
l2 ^ <*i1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
<*l1*> ^ (l2 ^ <*i1*>) is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((<*l1*> ^ (l2 ^ <*i1*>)),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((l2 ^ <*i1*>),(l1 . I)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ ((l2 ^ <*i1*>),(l1 . I)) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (l2,(l1 . I)) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len <*l1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (<*l1*> ^ l2) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len <*I*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom (l2,(l1 . I)) is V92() Element of bool NAT
1 + (len (<*l1*> ^ l2)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((<*l1*> ^ l2),I) . (1 + (len (<*l1*> ^ l2))) is set
(l2,(l1 . I)) . ((len l2) + 1) is set
(<*l1*> ^ l2) ^ <*i1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(((<*l1*> ^ l2) ^ <*i1*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(len (<*l1*> ^ l2)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((<*l1*> ^ l2),I) . ((len (<*l1*> ^ l2)) + 1) is set
i1 . (((<*l1*> ^ l2),I) . ((len (<*l1*> ^ l2)) + 1)) is set
<*(i1 . (((<*l1*> ^ l2),I) . ((len (<*l1*> ^ l2)) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((<*l1*> ^ l2),I) ^ <*(i1 . (((<*l1*> ^ l2),I) . ((len (<*l1*> ^ l2)) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i1 . ((l2,(l1 . I)) . ((len l2) + 1)) is set
<*(i1 . ((l2,(l1 . I)) . ((len l2) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(<*I*> ^ (l2,(l1 . I))) ^ <*(i1 . ((l2,(l1 . I)) . ((len l2) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(l2,(l1 . I)) ^ <*(i1 . ((l2,(l1 . I)) . ((len l2) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ ((l2,(l1 . I)) ^ <*(i1 . ((l2,(l1 . I)) . ((len l2) + 1)))*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*l1*> ^ {} is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
{} ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((<*l1*> ^ {}),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
({},I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
({},I) . (0 + 1) is set
l1 . (({},I) . (0 + 1)) is set
<*(l1 . (({},I) . (0 + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
({},I) ^ <*(l1 . (({},I) . (0 + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
({},I) . 1 is set
l1 . (({},I) . 1) is set
<*(l1 . (({},I) . 1))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(l1 . (({},I) . 1))*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*I*> . 1 is set
l1 . (<*I*> . 1) is set
<*(l1 . (<*I*> . 1))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(l1 . (<*I*> . 1))*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*(l1 . I)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(l1 . I)*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
({},(l1 . I)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ ({},(l1 . I)) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like Function-like set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
(I,<*X*>) is Relation-like Function-like set
(id I) (#) X is Relation-like I -defined Function-like set
{} ^ <*X*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,{}) is Relation-like Function-like set
(I,{}) (#) X is Relation-like Function-like set
I is set
X is Relation-like Function-like set
proj1 X is set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
(I,<*X*>) is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
(id I) (#) X is Relation-like I -defined Function-like set
I is set
X is Relation-like Function-like set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
(<*X*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X . I is set
<*I,(X . I)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*I*> . (0 + 1) is set
({},I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
{} ^ <*X*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(({} ^ <*X*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*(X . I)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(X . I)*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I is set
X is set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,l1) is Relation-like Function-like set
proj2 (I,l1) is set
l2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
l1 ^ l2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(l1 ^ l2)) is Relation-like Function-like set
(X,l2) is Relation-like Function-like set
(I,l1) (#) (X,l2) is Relation-like Function-like set
i1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
l1 ^ i1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(l1 ^ i1)) is Relation-like Function-like set
(X,i1) is Relation-like Function-like set
(I,l1) (#) (X,i1) is Relation-like Function-like set
i2 is Relation-like Function-like set
<*i2*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
i1 ^ <*i2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
l1 ^ (i1 ^ <*i2*>) is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(l1 ^ (i1 ^ <*i2*>))) is Relation-like Function-like set
(X,(i1 ^ <*i2*>)) is Relation-like Function-like set
(I,l1) (#) (X,(i1 ^ <*i2*>)) is Relation-like Function-like set
(l1 ^ i1) ^ <*i2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,((l1 ^ i1) ^ <*i2*>)) is Relation-like Function-like set
(I,(l1 ^ i1)) (#) i2 is Relation-like Function-like set
(X,i1) (#) i2 is Relation-like Function-like set
(I,l1) (#) ((X,i1) (#) i2) is Relation-like Function-like set
l1 ^ {} is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(l1 ^ {})) is Relation-like Function-like set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(I,l1) (#) (id X) is Relation-like X -valued Function-like set
(X,{}) is Relation-like Function-like set
(I,l1) (#) (X,{}) is Relation-like Function-like set
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(X,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,I) . ((len X) + 1) is set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ l1),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X ^ l1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ l1)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ l1),I) . ((len (X ^ l1)) + 1) is set
(l1,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,((X,I) . ((len X) + 1))) . ((len l1) + 1) is set
i1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ i1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ i1),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X ^ i1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ i1)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ i1),I) . ((len (X ^ i1)) + 1) is set
(i1,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len i1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(i1,((X,I) . ((len X) + 1))) . ((len i1) + 1) is set
i2 is Relation-like Function-like set
<*i2*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
i1 ^ <*i2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ (i1 ^ <*i2*>) is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ (i1 ^ <*i2*>)),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X ^ (i1 ^ <*i2*>)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ (i1 ^ <*i2*>))) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ (i1 ^ <*i2*>)),I) . ((len (X ^ (i1 ^ <*i2*>))) + 1) is set
((i1 ^ <*i2*>),((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (i1 ^ <*i2*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (i1 ^ <*i2*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((i1 ^ <*i2*>),((X,I) . ((len X) + 1))) . ((len (i1 ^ <*i2*>)) + 1) is set
len <*i2*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X ^ i1) ^ <*i2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
len ((X ^ i1) ^ <*i2*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . ((i1,((X,I) . ((len X) + 1))) . ((len i1) + 1)) is set
<*(i2 . ((i1,((X,I) . ((len X) + 1))) . ((len i1) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(i1,((X,I) . ((len X) + 1))) ^ <*(i2 . ((i1,((X,I) . ((len X) + 1))) . ((len i1) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (i1,((X,I) . ((len X) + 1))) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len ((X ^ i1),I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(((X ^ i1) ^ <*i2*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i2 . (((X ^ i1),I) . ((len (X ^ i1)) + 1)) is set
<*(i2 . (((X ^ i1),I) . ((len (X ^ i1)) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((X ^ i1),I) ^ <*(i2 . (((X ^ i1),I) . ((len (X ^ i1)) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
({},((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*((X,I) . ((len X) + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X ^ {} is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ {}),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X ^ {}) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ {})) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ {}),I) . ((len (X ^ {})) + 1) is set
len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
(len {}) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
({},((X,I) . ((len X) + 1))) . ((len {}) + 1) is set
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(X,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,I) . ((len X) + 1) is set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ l1),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(l1,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(X,I) $^ (l1,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X,I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i1 is set
<*i1*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
l2 ^ <*i1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ i2 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ i2),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(i2,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(X,I) $^ (i2,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (X ^ i2) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ i2)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((X ^ i2),I) . ((len (X ^ i2)) + 1) is set
len i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len i2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(i2,((X,I) . ((len X) + 1))) . ((len i2) + 1) is set
B is Relation-like Function-like set
<*B*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
i2 ^ <*B*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
X ^ (i2 ^ <*B*>) is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ (i2 ^ <*B*>)),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((i2 ^ <*B*>),((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(X,I) $^ ((i2 ^ <*B*>),((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (i2,((X,I) . ((len X) + 1))) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len ((i2 ^ <*B*>),((X,I) . ((len X) + 1))) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len (i2 ^ <*B*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (i2 ^ <*B*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X ^ i2) ^ <*B*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(((X ^ i2) ^ <*B*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)) is set
<*(B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((X ^ i2),I) ^ <*(B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l2 ^ (i2,((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(l2 ^ (i2,((X,I) . ((len X) + 1)))) ^ <*(B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(i2,((X,I) . ((len X) + 1))) ^ <*(B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l2 ^ ((i2,((X,I) . ((len X) + 1))) ^ <*(B . (((X ^ i2),I) . ((len (X ^ i2)) + 1)))*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l2 ^ ((i2 ^ <*B*>),((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*i1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X ^ {} is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((X ^ {}),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*((X,I) . ((len X) + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(X,I) $^ <*((X,I) . ((len X) + 1))*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
({},((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(X,I) $^ ({},((X,I) . ((len X) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
<*X,l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 -element FinSequence-like FinSubsequence-like set
(I,<*X,l1*>) is Relation-like Function-like set
X (#) l1 is Relation-like Function-like set
(id I) (#) (X (#) l1) is Relation-like I -defined Function-like set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*X*> ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,<*X*>) is Relation-like Function-like set
(I,<*X*>) (#) l1 is Relation-like Function-like set
(id I) (#) X is Relation-like I -defined Function-like set
((id I) (#) X) (#) l1 is Relation-like I -defined Function-like set
I is set
X is Relation-like Function-like set
proj1 X is set
l1 is Relation-like Function-like set
X (#) l1 is Relation-like Function-like set
proj1 (X (#) l1) is set
<*X,l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 -element FinSequence-like FinSubsequence-like set
(I,<*X,l1*>) is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
(id I) (#) (X (#) l1) is Relation-like I -defined Function-like set
(id I) (#) X is Relation-like I -defined Function-like set
((id I) (#) X) (#) l1 is Relation-like I -defined Function-like set
I is set
X is Relation-like Function-like set
X . I is set
l1 is Relation-like Function-like set
<*X,l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 -element FinSequence-like FinSubsequence-like set
(<*X,l1*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l1 . (X . I) is set
<*I,(X . I),(l1 . (X . I))*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
(<*X*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I,(X . I)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
len <*X*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*X*> ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((<*X*> ^ <*l1*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*I,(X . I)*> . (1 + 1) is set
l1 . (<*I,(X . I)*> . (1 + 1)) is set
<*(l1 . (<*I,(X . I)*> . (1 + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I,(X . I)*> ^ <*(l1 . (<*I,(X . I)*> . (1 + 1)))*> is non empty Relation-like NAT -defined Function-like finite 2 + 1 -element FinSequence-like FinSubsequence-like set
2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*(l1 . (X . I))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I,(X . I)*> ^ <*(l1 . (X . I))*> is non empty Relation-like NAT -defined Function-like finite 2 + 1 -element FinSequence-like FinSubsequence-like set
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
l2 is Relation-like Function-like set
<*X,l1,l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 3 -element FinSequence-like FinSubsequence-like set
(I,<*X,l1,l2*>) is Relation-like Function-like set
l1 (#) l2 is Relation-like Function-like set
X (#) (l1 (#) l2) is Relation-like Function-like set
(id I) (#) (X (#) (l1 (#) l2)) is Relation-like I -defined Function-like set
<*X,l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 -element FinSequence-like FinSubsequence-like set
<*l2*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*X,l1*> ^ <*l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 + 1 -element FinSequence-like FinSubsequence-like set
2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,<*X,l1*>) is Relation-like Function-like set
(I,<*X,l1*>) (#) l2 is Relation-like Function-like set
X (#) l1 is Relation-like Function-like set
(id I) (#) (X (#) l1) is Relation-like I -defined Function-like set
((id I) (#) (X (#) l1)) (#) l2 is Relation-like I -defined Function-like set
(X (#) l1) (#) l2 is Relation-like Function-like set
(id I) (#) ((X (#) l1) (#) l2) is Relation-like I -defined Function-like set
I is set
X is Relation-like Function-like set
proj1 X is set
l1 is Relation-like Function-like set
X (#) l1 is Relation-like Function-like set
proj1 (X (#) l1) is set
l2 is Relation-like Function-like set
l1 (#) l2 is Relation-like Function-like set
X (#) (l1 (#) l2) is Relation-like Function-like set
proj1 (X (#) (l1 (#) l2)) is set
<*X,l1,l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 3 -element FinSequence-like FinSubsequence-like set
(I,<*X,l1,l2*>) is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
(id I) (#) X is Relation-like I -defined Function-like set
((id I) (#) X) (#) (l1 (#) l2) is Relation-like I -defined Function-like set
((id I) (#) X) (#) l1 is Relation-like I -defined Function-like set
(((id I) (#) X) (#) l1) (#) l2 is Relation-like I -defined Function-like set
(id I) (#) (X (#) l1) is Relation-like I -defined Function-like set
(X (#) l1) (#) l2 is Relation-like Function-like set
(id I) (#) (X (#) (l1 (#) l2)) is Relation-like I -defined Function-like set
I is set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X is Relation-like Function-like set
X . I is set
l1 is Relation-like Function-like set
l1 . (X . I) is set
l2 is Relation-like Function-like set
<*X,l1,l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 3 -element FinSequence-like FinSubsequence-like set
(<*X,l1,l2*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
l2 . (l1 . (X . I)) is set
<*(X . I),(l1 . (X . I)),(l2 . (l1 . (X . I)))*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(X . I),(l1 . (X . I)),(l2 . (l1 . (X . I)))*> is non empty Relation-like NAT -defined Function-like finite 1 + 3 -element FinSequence-like FinSubsequence-like set
1 + 3 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*X,l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 -element FinSequence-like FinSubsequence-like set
(<*X,l1*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I,(X . I),(l1 . (X . I))*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set
len <*X,l1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*l2*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
<*X,l1*> ^ <*l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite 2 + 1 -element FinSequence-like FinSubsequence-like set
2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((<*X,l1*> ^ <*l2*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*I,(X . I),(l1 . (X . I))*> . (2 + 1) is set
l2 . (<*I,(X . I),(l1 . (X . I))*> . (2 + 1)) is set
<*(l2 . (<*I,(X . I),(l1 . (X . I))*> . (2 + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I,(X . I),(l1 . (X . I))*> ^ <*(l2 . (<*I,(X . I),(l1 . (X . I))*> . (2 + 1)))*> is non empty Relation-like NAT -defined Function-like finite 3 + 1 -element FinSequence-like FinSubsequence-like set
3 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*(l2 . (l1 . (X . I)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*I,(X . I),(l1 . (X . I))*> ^ <*(l2 . (l1 . (X . I)))*> is non empty Relation-like NAT -defined Function-like finite 3 + 1 -element FinSequence-like FinSubsequence-like set
<*(X . I),(l1 . (X . I))*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*I*> ^ <*(X . I),(l1 . (X . I))*> is non empty Relation-like NAT -defined Function-like finite 1 + 2 -element FinSequence-like FinSubsequence-like set
1 + 2 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(<*I*> ^ <*(X . I),(l1 . (X . I))*>) ^ <*(l2 . (l1 . (X . I)))*> is non empty Relation-like NAT -defined Function-like finite (1 + 2) + 1 -element FinSequence-like FinSubsequence-like set
(1 + 2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
<*(X . I),(l1 . (X . I))*> ^ <*(l2 . (l1 . (X . I)))*> is non empty Relation-like NAT -defined Function-like finite 2 + 1 -element FinSequence-like FinSubsequence-like set
<*I*> ^ (<*(X . I),(l1 . (X . I))*> ^ <*(l2 . (l1 . (X . I)))*>) is non empty Relation-like NAT -defined Function-like finite 1 + (2 + 1) -element FinSequence-like FinSubsequence-like set
1 + (2 + 1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I . 1 is set
proj1 (I . 1) is set
l1 is set
l2 is set
i1 is set
i2 is set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . (len I) is set
proj2 (I . (len I)) is set
l1 is set
l2 is set
i1 is set
i2 is set
({}) is set
({}) is set
I is Relation-like Function-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
proj1 I is set
proj2 I is set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I*> ^ X is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((<*I*> ^ X)) is set
X ^ <*I*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((X ^ <*I*>)) is set
(<*I*> ^ X) . 1 is set
proj1 ((<*I*> ^ X) . 1) is set
len <*I*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (X ^ <*I*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X ^ <*I*>) . ((len X) + 1) is set
proj2 ((X ^ <*I*>) . ((len X) + 1)) is set
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,X) is Relation-like Function-like set
proj2 (I,X) is set
(X) is set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
X ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(X ^ <*l1*>)) is Relation-like Function-like set
proj2 (I,(X ^ <*l1*>)) is set
((X ^ <*l1*>)) is set
(I,X) (#) l1 is Relation-like Function-like set
proj2 l1 is set
(I,{}) is Relation-like Function-like set
proj2 (I,{}) is set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I ^ X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (I ^ X) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len (I ^ X)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom (I ^ X) is V92() Element of bool NAT
l1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
Seg ((len I) + 1) is non empty finite (len I) + 1 -element Element of bool NAT
l1 | (Seg ((len I) + 1)) is Relation-like NAT -defined Seg ((len I) + 1) -defined NAT -defined Function-like FinSubsequence-like set
Seg (len I) is finite len I -element Element of bool NAT
l1 | (Seg (len I)) is Relation-like NAT -defined Seg (len I) -defined NAT -defined Function-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + (len X) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
(I ^ X) . B is set
I . B is set
l1 . B is set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (B + 1) is set
Funcs ((l1 . B),(l1 . (B + 1))) is functional set
dom i2 is V92() Element of bool NAT
i2 . B is set
i2 . (B + 1) is set
Funcs ((i2 . B),(i2 . (B + 1))) is functional set
i2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i1 ^ i2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom X is V92() Element of bool NAT
(len i1) + (len i2) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X . B is set
i2 . B is set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . (B + 1) is set
Funcs ((i2 . B),(i2 . (B + 1))) is functional set
(len I) + B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I ^ X) . ((len I) + B) is set
l1 . ((len I) + B) is set
((len I) + B) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (((len I) + B) + 1) is set
Funcs ((l1 . ((len I) + B)),(l1 . (((len I) + B) + 1))) is functional set
(len I) + ((len X) + 1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + (len i2) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom i2 is V92() Element of bool NAT
(len I) + (B + 1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . ((len I) + (B + 1)) is set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is set
proj1 I is V92() set
I . l1 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . l2 is set
X . l2 is set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X . (l2 + 1) is set
Funcs ((X . l2),(X . (l2 + 1))) is functional set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*{}*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
X is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
len X is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . l1 is set
X . l1 is Relation-like Function-like set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X . (l1 + 1) is Relation-like Function-like set
Funcs ((X . l1),(X . (l1 + 1))) is functional set
I is Relation-like Function-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like set
proj1 I is set
proj2 I is set
<*(proj1 I),(proj2 I)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
X is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
len X is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len <*I*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len <*I*>) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom <*I*> is non empty trivial 1 -element V92() Element of bool NAT
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
<*I*> . l2 is Relation-like Function-like set
X . l2 is set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X . (l2 + 1) is set
Funcs ((X . l2),(X . (l2 + 1))) is functional set
{1} is non empty trivial 1 -element Element of bool NAT
the non empty Relation-like Function-like set is non empty Relation-like Function-like set
<* the non empty Relation-like Function-like set *> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
X is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
l1 is set
proj1 X is non empty trivial 1 -element V92() set
X . l1 is Relation-like Function-like set
dom X is non empty trivial 1 -element V92() Element of bool NAT
{1} is non empty trivial 1 -element Element of bool NAT
I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,X) is Relation-like Function-like set
proj1 (I,X) is set
(X) is set
(X) /\ I is set
l1 is Relation-like Function-like set
<*l1*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
X ^ <*l1*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(I,(X ^ <*l1*>)) is Relation-like Function-like set
proj1 (I,(X ^ <*l1*>)) is set
((X ^ <*l1*>)) is set
((X ^ <*l1*>)) /\ I is set
(I,X) (#) l1 is Relation-like Function-like set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
(id I) (#) l1 is Relation-like I -defined Function-like set
<*l1*> ^ {} is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
proj1 l1 is set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is set
<*l2*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
i1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*l2*> ^ i1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len i1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X . 1 is Relation-like Function-like set
proj1 l2 is set
dom X is V92() Element of bool NAT
(X ^ <*l1*>) . (len X) is Relation-like Function-like set
X . (len X) is Relation-like Function-like set
proj2 (I,X) is set
(X) is set
len (X ^ <*l1*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (X ^ <*l1*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom (X ^ <*l1*>) is non empty V92() Element of bool NAT
i2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is set
<*B*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
B ^ <*B*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*l1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . (len X) is set
i2 . ((len X) + 1) is set
Funcs ((i2 . (len X)),(i2 . ((len X) + 1))) is functional set
len <*B*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len B) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
e is Relation-like Function-like set
proj1 e is set
proj2 e is set
i1 ^ <*l1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*l2*> ^ (i1 ^ <*l1*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*l2*> ^ (i1 ^ <*l1*>)) . 1 is set
(X ^ <*l1*>) . ((len X) + 1) is Relation-like Function-like set
((len X) + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . (((len X) + 1) + 1) is set
Funcs ((i2 . ((len X) + 1)),(i2 . (((len X) + 1) + 1))) is functional set
l is Relation-like Function-like set
proj1 l is set
proj2 l is set
(I,{}) is Relation-like Function-like set
proj1 (I,{}) is set
({}) /\ I is set
X is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () set
(I,X) is Relation-like Function-like set
proj1 (I,X) is set
(X) is set
(X) /\ I is set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () set
(I) is set
((I),I) is Relation-like Function-like set
proj1 ((I),I) is set
id (I) is Relation-like (I) -defined (I) -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(I),(I):]
[:(I),(I):] is Relation-like set
bool [:(I),(I):] is non empty set
(I) /\ (I) is set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () set
(I) is set
X is Relation-like Function-like set
proj2 X is set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
<*X*> ^ I is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
l1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
proj1 X is set
<*(proj1 X)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*(proj1 X)*> ^ l1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*(proj1 X)*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len <*X*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (<*X*> ^ I) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . 1 is Relation-like Function-like set
l1 . 1 is set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (1 + 1) is set
Funcs ((l1 . 1),(l1 . (1 + 1))) is functional set
l1 . 2 is set
i1 is Relation-like Function-like set
proj1 i1 is set
proj2 i1 is set
len (<*(proj1 X)*> ^ l1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (<*X*> ^ I)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom (<*X*> ^ I) is non empty V92() Element of bool NAT
dom l1 is V92() Element of bool NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(<*X*> ^ I) . i1 is Relation-like Function-like set
(<*(proj1 X)*> ^ l1) . i1 is set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(<*(proj1 X)*> ^ l1) . (i1 + 1) is set
Funcs (((<*(proj1 X)*> ^ l1) . i1),((<*(proj1 X)*> ^ l1) . (i1 + 1))) is functional set
i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(1 + 1) + i2 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(i2 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (i2 + 1) is Relation-like Function-like set
l1 . (i2 + 1) is set
l1 . ((i2 + 1) + 1) is set
Funcs ((l1 . (i2 + 1)),(l1 . ((i2 + 1) + 1))) is functional set
I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () set
(I) is set
X is Relation-like Function-like set
proj1 X is set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
I ^ <*X*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len I) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom I is V92() Element of bool NAT
l1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i1 is set
<*i1*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
l2 ^ <*i1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I . (len I) is Relation-like Function-like set
l1 . (len I) is set
l1 . ((len I) + 1) is set
Funcs ((l1 . (len I)),(l1 . ((len I) + 1))) is functional set
i2 is Relation-like Function-like set
proj1 i2 is set
proj2 i2 is set
Funcs ((l1 . (len I)),(proj1 X)) is functional set
proj2 X is set
<*(proj1 X),(proj2 X)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*(proj1 X),(proj2 X)*> . 1 is set
<*(proj1 X),(proj2 X)*> . 2 is set
len <*X*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (I ^ <*X*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l2 ^ <*(proj1 X),(proj2 X)*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*(proj1 X),(proj2 X)*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (l2 ^ <*(proj1 X),(proj2 X)*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len l2) + (1 + 1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom <*(proj1 X),(proj2 X)*> is non empty 2 -element V92() Element of bool NAT
len <*i1*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len l2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (I ^ <*X*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom (I ^ <*X*>) is non empty V92() Element of bool NAT
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I ^ <*X*>) . B is Relation-like Function-like set
(l2 ^ <*(proj1 X),(proj2 X)*>) . B is set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l2 ^ <*(proj1 X),(proj2 X)*>) . (B + 1) is set
Funcs (((l2 ^ <*(proj1 X),(proj2 X)*>) . B),((l2 ^ <*(proj1 X),(proj2 X)*>) . (B + 1))) is functional set
dom l2 is V92() Element of bool NAT
l2 . B is set
l1 . B is set
dom l2 is V92() Element of bool NAT
l1 . B is set
l2 . B is set
I . B is Relation-like Function-like set
l1 . (B + 1) is set
Funcs ((l1 . B),(l1 . (B + 1))) is functional set
l2 . (B + 1) is set
I is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
dom (id X) is Element of bool X
bool X is non empty set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
(l1) is set
(l1,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,I) . ((len l1) + 1) is set
(X,l1) is Relation-like Function-like set
(X,l1) . I is set
l2 is Relation-like Function-like set
<*l2*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
l1 ^ <*l2*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((l1 ^ <*l2*>)) is set
((l1 ^ <*l2*>),I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (l1 ^ <*l2*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (l1 ^ <*l2*>)) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((l1 ^ <*l2*>),I) . ((len (l1 ^ <*l2*>)) + 1) is set
(X,(l1 ^ <*l2*>)) is Relation-like Function-like set
(X,(l1 ^ <*l2*>)) . I is set
(id X) . I is set
(id X) (#) l2 is Relation-like X -defined Function-like set
((id X) (#) l2) . I is set
l2 . I is set
len <*l2*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,l1) (#) l2 is Relation-like Function-like set
(<*l2*>,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*I,(l2 . I)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
(X,<*l2*>) is Relation-like Function-like set
l2 . ((l1,I) . ((len l1) + 1)) is set
<*(l2 . ((l1,I) . ((len l1) + 1)))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(l1,I) ^ <*(l2 . ((l1,I) . ((len l1) + 1)))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 (X,l1) is set
(l1) /\ X is set
(l1 ^ <*l2*>) . 1 is Relation-like Function-like set
proj1 ((l1 ^ <*l2*>) . 1) is set
l1 . 1 is Relation-like Function-like set
proj1 (l1 . 1) is set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom l1 is V92() Element of bool NAT
len (l1,I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 . ((X,l1) . I) is set
({},I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered () Element of NAT
(len {}) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
({},I) . ((len {}) + 1) is set
(X,{}) is Relation-like Function-like set
(X,{}) . I is set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () set
(l1) is set
(l1,I) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,I) . ((len l1) + 1) is set
(X,l1) is Relation-like Function-like set
(X,l1) . I is set
X is set
I is set
[:I,X:] is Relation-like set
bool [:I,X:] is non empty set
the Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:] is Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:]
<* the Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:]*> is non empty trivial Relation-like NAT -defined bool [:I,X:] -valued Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () FinSequence of bool [:I,X:]
l2 is non empty trivial Relation-like NAT -defined bool [:I,X:] -valued Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () FinSequence of bool [:I,X:]
(l2) is set
(l2) is set
l2 ^ {} is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
{} ^ l2 is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom the Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:] is Element of bool I
bool I is non empty set
rng the Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:] is Element of bool X
bool X is non empty set
X is set
I is non empty set
l1 is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () (X,I)
(X,l1) is Relation-like Function-like set
[:X,I:] is Relation-like set
bool [:X,I:] is non empty set
(l1) is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
proj2 (X,l1) is set
(l1) is set
proj1 (X,l1) is set
I is non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
Seg l1 is finite l1 -element Element of bool NAT
l2 is set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom I is non empty V92() Element of bool NAT
I . i1 is set
I . (i1 + 1) is set
i2 is non empty set
B is non empty set
[:i2,B:] is non empty Relation-like set
bool [:i2,B:] is non empty set
the non empty Relation-like i2 -defined B -valued Function-like total quasi_total Element of bool [:i2,B:] is non empty Relation-like i2 -defined B -valued Function-like total quasi_total Element of bool [:i2,B:]
Funcs ((I . i1),(I . (i1 + 1))) is functional set
l2 is Relation-like Function-like set
proj1 l2 is set
i1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len i1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom i1 is V92() Element of bool NAT
i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 . i2 is set
I . i2 is set
i2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (i2 + 1) is set
Funcs ((I . i2),(I . (i2 + 1))) is functional set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I . B is set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (B + 1) is set
Funcs ((I . B),(I . (B + 1))) is functional set
I is non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like (I)
len I is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom X is V92() Element of bool NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X . l1 is set
I . l1 is set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (l1 + 1) is set
Funcs ((I . l1),(I . (l1 + 1))) is functional set
l1 is set
proj1 X is V92() set
X . l1 is set
dom X is V92() Element of bool NAT
len I is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom I is non empty V92() Element of bool NAT
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . l2 is set
I . (l2 + 1) is set
X . l2 is set
i1 is non empty set
i2 is non empty set
Funcs (i1,i2) is non empty functional FUNCTION_DOMAIN of i1,i2
B is Relation-like Function-like set
proj1 B is set
proj2 B is set
I is non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I . 1 is set
len I is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (len I) is set
X is Relation-like non-empty NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () (I)
(X) is set
(X) is set
dom X is V92() Element of bool NAT
X . 1 is Relation-like Function-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (1 + 1) is set
Funcs ((I . 1),(I . (1 + 1))) is functional set
I . 2 is set
l1 is Relation-like Function-like set
proj1 l1 is set
proj2 l1 is set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X . (len X) is Relation-like Function-like set
I . (len X) is set
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . ((len X) + 1) is set
Funcs ((I . (len X)),(I . ((len X) + 1))) is functional set
l1 is Relation-like Function-like set
proj1 l1 is set
proj2 l1 is set
I is non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
I . 1 is set
len I is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I . (len I) is set
X is Relation-like non-empty NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like () (I)
((I . 1),X) is Relation-like Function-like set
proj1 ((I . 1),X) is set
proj2 ((I . 1),X) is set
len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
id (I . 1) is Relation-like I . 1 -defined I . 1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(I . 1),(I . 1):]
[:(I . 1),(I . 1):] is Relation-like set
bool [:(I . 1),(I . 1):] is non empty set
(X) is set
(X) is set
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty Element of bool (bool [:I,I:])
bool [:I,I:] is non empty set
bool (bool [:I,I:]) is non empty set
[:NAT,(bool [:I,I:]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:I,I:]):] is non empty non finite set
X is non empty Relation-like NAT -defined bool [:I,I:] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:I,I:]):]
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X . l1 is set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X . l2 is Relation-like I -defined I -valued Element of bool [:I,I:]
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like I -defined I -valued Function-like total quasi_total Element of bool [:I,I:]
rng X is Element of bool I
bool I is non empty set
dom X is Element of bool I
I is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty Element of bool (bool [:(field I),(field I):])
bool [:(field I),(field I):] is non empty set
bool (bool [:(field I),(field I):]) is non empty set
[:NAT,(bool [:(field I),(field I):]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:(field I),(field I):]):] is non empty non finite set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
l1 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
l1 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l2 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
l2 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (i1 + 1) is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l1 . i1 is Relation-like set
I (#) (l1 . i1) is Relation-like set
i2 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
e is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
B is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
I (#) B is Relation-like field I -valued set
l is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l2 . (B + 1) is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l2 . B is Relation-like set
I (#) (l2 . B) is Relation-like set
I is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty Element of bool (bool [:(field I),(field I):])
bool [:(field I),(field I):] is non empty set
bool (bool [:(field I),(field I):]) is non empty set
[:NAT,(bool [:(field I),(field I):]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:(field I),(field I):]):] is non empty non finite set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
I (#) B is Relation-like field I -valued set
i2 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
e is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
i2 * e is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
i1 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
i2 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
i2 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
i2 . B is Relation-like set
B + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 . (B + 1) is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
I (#) (i2 . B) is Relation-like set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i2 . l1 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l1 is Relation-like set
i1 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
i1 . X is Relation-like set
i1 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l2 is Relation-like set
i2 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
i2 . X is Relation-like set
i2 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
I is Relation-like Function-like set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,X) is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty Element of bool (bool [:(field I),(field I):])
bool [:(field I),(field I):] is non empty set
bool (bool [:(field I),(field I):]) is non empty set
[:NAT,(bool [:(field I),(field I):]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:(field I),(field I):]):] is non empty non finite set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
l1 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
l1 . X is Relation-like set
l1 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l1 . 0 is Relation-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 . l2 is Relation-like set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
l1 . (l2 + 1) is Relation-like set
l1 . (l2 + 1) is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
i1 is Relation-like Function-like set
I (#) i1 is Relation-like Function-like set
I is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty set
(id (field I)) (#) I is Relation-like field I -defined set
I (#) (id (field I)) is Relation-like field I -valued set
I is Relation-like set
(I,0) is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty set
bool [:(field I),(field I):] is non empty Element of bool (bool [:(field I),(field I):])
bool (bool [:(field I),(field I):]) is non empty set
[:NAT,(bool [:(field I),(field I):]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:(field I),(field I):]):] is non empty non finite set
X is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
X . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
I is Relation-like set
proj2 I is set
proj1 I is set
(I,0) is Relation-like set
id (proj1 I) is Relation-like proj1 I -defined proj1 I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 I),(proj1 I):]
[:(proj1 I),(proj1 I):] is Relation-like set
bool [:(proj1 I),(proj1 I):] is non empty set
field I is set
(proj1 I) \/ (proj2 I) is set
I is Relation-like set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(X + 1)) is Relation-like set
(I,X) is Relation-like set
I (#) (I,X) is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty Element of bool (bool [:(field I),(field I):])
bool [:(field I),(field I):] is non empty set
bool (bool [:(field I),(field I):]) is non empty set
[:NAT,(bool [:(field I),(field I):]):] is non empty Relation-like non finite set
bool [:NAT,(bool [:(field I),(field I):]):] is non empty non finite set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
l1 is non empty Relation-like NAT -defined bool [:(field I),(field I):] -valued Function-like total quasi_total Element of bool [:NAT,(bool [:(field I),(field I):]):]
l1 . (X + 1) is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l1 . 0 is Relation-like field I -defined field I -valued Element of bool [:(field I),(field I):]
l1 . X is Relation-like set
I (#) (l1 . X) is Relation-like set
I is Relation-like set
(I,1) is Relation-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(0 + 1)) is Relation-like set
(I,0) is Relation-like set
I (#) (I,0) is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty set
I (#) (id (field I)) is Relation-like field I -valued set
I is Relation-like set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(X + 1)) is Relation-like set
(I,X) is Relation-like set
(I,X) (#) I is Relation-like set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(l1 + 1)) is Relation-like set
(I,l1) is Relation-like set
(I,l1) (#) I is Relation-like set
(l1 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,((l1 + 1) + 1)) is Relation-like set
(I,(l1 + 1)) (#) I is Relation-like set
I (#) (I,l1) is Relation-like set
(I (#) (I,l1)) (#) I is Relation-like set
I (#) ((I,l1) (#) I) is Relation-like set
(l1 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,((l1 + 1) + 1)) is Relation-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(0 + 1)) is Relation-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty set
(id (field I)) (#) I is Relation-like field I -defined set
(I,0) is Relation-like set
(I,0) (#) I is Relation-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(0 + 1)) is Relation-like set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like set
(X,I) is Relation-like set
proj1 (X,I) is set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
proj2 (X,I) is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(X,l1) is Relation-like set
proj1 (X,l1) is set
proj2 (X,l1) is set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,(l1 + 1)) is Relation-like set
proj1 (X,(l1 + 1)) is set
proj2 (X,(l1 + 1)) is set
(X,l1) (#) X is Relation-like set
X (#) (X,l1) is Relation-like set
(X,0) is Relation-like set
id (field X) is Relation-like field X -defined field X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field X),(field X):]
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
proj1 (X,0) is set
proj2 (X,0) is set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like set
(X,I) is Relation-like set
proj1 (X,I) is set
proj1 X is set
proj2 (X,I) is set
proj2 X is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,(l1 + 1)) is Relation-like set
proj1 (X,(l1 + 1)) is set
proj2 (X,(l1 + 1)) is set
(l1 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,((l1 + 1) + 1)) is Relation-like set
proj1 (X,((l1 + 1) + 1)) is set
proj2 (X,((l1 + 1) + 1)) is set
(l1 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,((l1 + 1) + 1)) is Relation-like set
X (#) (X,(l1 + 1)) is Relation-like set
(X,(l1 + 1)) (#) X is Relation-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,(0 + 1)) is Relation-like set
proj1 (X,(0 + 1)) is set
proj2 (X,(0 + 1)) is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I is Relation-like set
proj2 I is set
proj1 I is set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,X) is Relation-like set
proj1 (I,X) is set
proj2 (I,X) is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,l1) is Relation-like set
proj1 (I,l1) is set
proj2 (I,l1) is set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(l1 + 1)) is Relation-like set
proj1 (I,(l1 + 1)) is set
proj2 (I,(l1 + 1)) is set
I (#) (I,l1) is Relation-like set
(I,l1) (#) I is Relation-like set
(I,0) is Relation-like set
id (proj1 I) is Relation-like proj1 I -defined proj1 I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 I),(proj1 I):]
[:(proj1 I),(proj1 I):] is Relation-like set
bool [:(proj1 I),(proj1 I):] is non empty set
proj1 (I,0) is set
proj2 (I,0) is set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
id (field X) is Relation-like field X -defined field X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field X),(field X):]
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
(X,I) is Relation-like set
(id (field X)) (#) (X,I) is Relation-like field X -defined set
proj1 (X,I) is set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like set
(X,I) is Relation-like set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
id (field X) is Relation-like field X -defined field X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field X),(field X):]
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
(X,I) (#) (id (field X)) is Relation-like field X -valued set
proj2 (X,I) is set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is Relation-like set
(l1,I) is Relation-like set
(l1,X) is Relation-like set
(l1,I) (#) (l1,X) is Relation-like set
(l1,(X + I)) is Relation-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,l2) is Relation-like set
(l1,l2) (#) (l1,X) is Relation-like set
X + l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X + l2)) is Relation-like set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(l2 + 1)) is Relation-like set
(l1,(l2 + 1)) (#) (l1,X) is Relation-like set
X + (l2 + 1) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X + (l2 + 1))) is Relation-like set
l1 (#) (l1,l2) is Relation-like set
(l1 (#) (l1,l2)) (#) (l1,X) is Relation-like set
l1 (#) ((l1,l2) (#) (l1,X)) is Relation-like set
(X + l2) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,((X + l2) + 1)) is Relation-like set
(l1,0) is Relation-like set
(l1,0) (#) (l1,X) is Relation-like set
field l1 is set
proj1 l1 is set
proj2 l1 is set
(proj1 l1) \/ (proj2 l1) is set
id (field l1) is Relation-like field l1 -defined field l1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field l1),(field l1):]
[:(field l1),(field l1):] is Relation-like set
bool [:(field l1),(field l1):] is non empty set
(id (field l1)) (#) (l1,X) is Relation-like field l1 -defined set
X + 0 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X + 0)) is Relation-like set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I * X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I * (X + 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is Relation-like set
(l1,I) is Relation-like set
((l1,I),X) is Relation-like set
(l1,(I * X)) is Relation-like set
((l1,I),(X + 1)) is Relation-like set
(l1,(I * (X + 1))) is Relation-like set
(l1,I) (#) ((l1,I),X) is Relation-like set
I * 1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I * X) + (I * 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,((I * X) + (I * 1))) is Relation-like set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X * I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is Relation-like set
(l1,X) is Relation-like set
((l1,X),I) is Relation-like set
(l1,(X * I)) is Relation-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((l1,X),(l2 + 1)) is Relation-like set
X * (l2 + 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X * (l2 + 1))) is Relation-like set
(l2 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((l1,X),((l2 + 1) + 1)) is Relation-like set
X * ((l2 + 1) + 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X * ((l2 + 1) + 1))) is Relation-like set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((l1,X),(0 + 1)) is Relation-like set
X * (0 + 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(X * (0 + 1))) is Relation-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I * X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is Relation-like set
proj2 l1 is set
proj1 l1 is set
(l1,I) is Relation-like set
((l1,I),X) is Relation-like set
(l1,(I * X)) is Relation-like set
proj1 (l1,I) is set
field (l1,I) is set
proj2 (l1,I) is set
(proj1 (l1,I)) \/ (proj2 (l1,I)) is set
((l1,I),0) is Relation-like set
id (proj1 l1) is Relation-like proj1 l1 -defined proj1 l1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 l1),(proj1 l1):]
[:(proj1 l1),(proj1 l1):] is Relation-like set
bool [:(proj1 l1),(proj1 l1):] is non empty set
field l1 is set
(proj1 l1) \/ (proj2 l1) is set
id (field l1) is Relation-like field l1 -defined field l1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field l1),(field l1):]
[:(field l1),(field l1):] is Relation-like set
bool [:(field l1),(field l1):] is non empty set
I * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered () Element of NAT
(l1,(I * 0)) is Relation-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
((l1,I),l2) is Relation-like set
I * l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(I * l2)) is Relation-like set
l2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((l1,I),(l2 + 1)) is Relation-like set
I * (l2 + 1) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(I * (l2 + 1))) is Relation-like set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
({},I) is Relation-like Function-like set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
({},X) is Relation-like Function-like set
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
({},(X + 1)) is Relation-like Function-like set
{} (#) ({},X) is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered () set
({},0) is Relation-like Function-like set
field {} is set
(proj1 {}) \/ (proj2 {}) is Relation-like NAT -defined set
id (field {}) is Relation-like field {} -defined field {} -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field {}),(field {}):]
[:(field {}),(field {}):] is Relation-like set
bool [:(field {}),(field {}):] is non empty set
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
((id I),X) is Relation-like Function-like set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
((id I),l1) is Relation-like Function-like set
l1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((id I),(l1 + 1)) is Relation-like Function-like set
(id I) (#) ((id I),l1) is Relation-like I -defined Function-like set
field (id I) is set
proj1 (id I) is set
proj2 (id I) is set
(proj1 (id I)) \/ (proj2 (id I)) is set
id (field (id I)) is Relation-like field (id I) -defined field (id I) -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field (id I)),(field (id I)):]
[:(field (id I)),(field (id I)):] is Relation-like set
bool [:(field (id I)),(field (id I)):] is non empty set
((id I),0) is Relation-like Function-like set
I is Relation-like set
proj2 I is set
proj1 I is set
(I,2) is Relation-like set
1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(1 + 1)) is Relation-like set
(I,1) is Relation-like set
(I,1) (#) I is Relation-like set
I (#) I is Relation-like set
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
l1 is Relation-like I -defined I -valued Function-like total quasi_total Element of bool [:I,I:]
(l1,X) is Relation-like Function-like set
dom l1 is Element of bool I
bool I is non empty set
rng l1 is Element of bool I
proj1 (l1,X) is set
proj2 (l1,X) is set
l2 is Relation-like I -defined I -valued Element of bool [:I,I:]
dom l2 is Element of bool I
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
X is Relation-like I -defined I -valued Function-like total quasi_total Element of bool [:I,I:]
(X,0) is Relation-like Function-like set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
id (field X) is Relation-like field X -defined field X -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field X),(field X):]
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
dom X is Element of bool I
bool I is non empty set
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X * l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Relation-like I -defined I -valued Function-like total quasi_total Element of bool [:I,I:]
(l2,X) is Relation-like Function-like set
((l2,X),l1) is Relation-like Function-like set
(l2,(X * l1)) is Relation-like Function-like set
rng l2 is Element of bool I
bool I is non empty set
dom l2 is Element of bool I
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is Relation-like I -defined I -valued Function-like Element of bool [:I,I:]
(l1,X) is Relation-like Function-like set
field l1 is set
proj1 l1 is set
proj2 l1 is set
(proj1 l1) \/ (proj2 l1) is set
dom l1 is Element of bool I
bool I is non empty set
rng l1 is Element of bool I
(dom l1) \/ (rng l1) is Element of bool I
proj2 (l1,X) is set
proj1 (l1,X) is set
I is set
X is set
X --> I is Relation-like X -defined {I} -valued Function-like constant total quasi_total Element of bool [:X,{I}:]
{I} is non empty trivial 1 -element set
[:X,{I}:] is Relation-like set
bool [:X,{I}:] is non empty set
l1 is Relation-like Function-like set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(l1,l2) is Relation-like Function-like set
proj1 l1 is set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(i1 + 1)) is Relation-like Function-like set
i2 is set
l1 . i2 is set
(i1 + 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,((i1 + 1) + 1)) is Relation-like Function-like set
(l1,((i1 + 1) + 1)) . i2 is set
l1 (#) l1 is Relation-like Function-like set
(l1 (#) l1) . i2 is set
l1 . (l1 . i2) is set
proj2 l1 is set
proj1 (l1,((i1 + 1) + 1)) is set
0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(l1,(0 + 1)) is Relation-like Function-like set
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
i2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i2 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
I is Relation-like Function-like set
field I is set
proj1 I is set
proj2 I is set
(proj1 I) \/ (proj2 I) is set
X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(I,X) is Relation-like Function-like set
X |-> I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
Seg X is finite X -element Element of bool NAT
(Seg X) --> I is Relation-like Seg X -defined {I} -valued Function-like constant total quasi_total Function-yielding V41() Element of bool [:(Seg X),{I}:]
{I} is non empty trivial functional 1 -element set
[:(Seg X),{I}:] is Relation-like set
bool [:(Seg X),{I}:] is non empty set
((field I),(X |-> I)) is Relation-like Function-like set
X + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I,(X + 1)) is Relation-like Function-like set
((field I),(X |-> I)) (#) I is Relation-like Function-like set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant Function-yielding V41() finite 1 -element FinSequence-like FinSubsequence-like () set
(X |-> I) ^ <*I*> is non empty Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
((field I),((X |-> I) ^ <*I*>)) is Relation-like Function-like set
(X + 1) |-> I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
Seg (X + 1) is non empty finite X + 1 -element Element of bool NAT
(Seg (X + 1)) --> I is non empty Relation-like Seg (X + 1) -defined {I} -valued Function-like constant total quasi_total Function-yielding V41() Element of bool [:(Seg (X + 1)),{I}:]
[:(Seg (X + 1)),{I}:] is non empty Relation-like set
bool [:(Seg (X + 1)),{I}:] is non empty set
((field I),((X + 1) |-> I)) is Relation-like Function-like set
(I,0) is Relation-like Function-like set
id (field I) is Relation-like field I -defined field I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(field I),(field I):]
[:(field I),(field I):] is Relation-like set
bool [:(field I),(field I):] is non empty set
((field I),{}) is Relation-like Function-like set
0 |-> I is Relation-like NAT -defined Function-like Function-yielding V41() finite FinSequence-like FinSubsequence-like set
Seg 0 is empty proper Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered () Element of bool NAT
(Seg 0) --> I is empty Relation-like non-empty empty-yielding Seg 0 -defined {I} -valued Function-like one-to-one constant functional total V18() V19() V20() V22() V23() V24() quasi_total ext-real non positive non negative V37() V38() V39() Function-yielding V41() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered () Element of bool [:(Seg 0),{I}:]
[:(Seg 0),{I}:] is Relation-like set
bool [:(Seg 0),{I}:] is non empty set
((field I),(0 |-> I)) is Relation-like Function-like set
X is Relation-like Function-like set
I is Relation-like Function-like set
proj1 X is set
l1 is set
l2 is set
(I,l1,l2) is Relation-like Function-like set
i1 is set
X . i1 is set
I . i1 is set
(I,l1,l2) . i1 is set
proj1 I is set
proj1 (I,l1,l2) is set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is set
I | l1 is Relation-like Function-like set
X | l1 is Relation-like Function-like set
proj1 I is set
(proj1 I) \/ l1 is set
I | ((proj1 I) \/ l1) is Relation-like Function-like set
(proj1 I) \ l1 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
((proj1 I) \ l1) \/ l1 is set
I | (((proj1 I) \ l1) \/ l1) is Relation-like Function-like set
I | ((proj1 I) \ l1) is Relation-like Function-like set
(I | ((proj1 I) \ l1)) \/ (I | l1) is Relation-like set
proj1 X is set
(proj1 X) \ l1 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
X | ((proj1 X) \ l1) is Relation-like Function-like set
(X | ((proj1 X) \ l1)) \/ (X | l1) is Relation-like set
((proj1 X) \ l1) \/ l1 is set
X | (((proj1 X) \ l1) \/ l1) is Relation-like Function-like set
(proj1 X) \/ l1 is set
X | ((proj1 X) \/ l1) is Relation-like Function-like set
I is Relation-like Function-like set
X is set
l2 is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj1 I is set
{X} is non empty trivial 1 -element set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
dom (X .--> l1) is non empty trivial 1 -element Element of bool {X}
bool {X} is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
X is set
l2 is set
l1 is set
(I,X,l1) is Relation-like Function-like set
(I,X,l1) | l2 is Relation-like Function-like set
I | l2 is Relation-like Function-like set
proj1 I is set
{X} is non empty trivial 1 -element set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
dom (X .--> l1) is non empty trivial 1 -element Element of bool {X}
bool {X} is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
(I +* (X .--> l1)) | l2 is Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
X is Relation-like Function-like set
i1 is set
I | i1 is Relation-like Function-like set
X | i1 is Relation-like Function-like set
l1 is set
l2 is set
(I,l1,l2) is Relation-like Function-like set
(I,l1,l2) | i1 is Relation-like Function-like set
(X,l1,l2) is Relation-like Function-like set
(X,l1,l2) | i1 is Relation-like Function-like set
proj1 X is set
proj1 I is set
(proj1 I) /\ i1 is set
proj1 (X | i1) is set
(proj1 X) /\ i1 is set
l1 .--> l2 is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
{l2} is non empty trivial 1 -element set
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
I +* (l1 .--> l2) is non empty Relation-like Function-like set
(I +* (l1 .--> l2)) | i1 is Relation-like Function-like set
(l1 .--> l2) | i1 is Relation-like i1 -defined {l1} -defined Function-like constant set
(X | i1) +* ((l1 .--> l2) | i1) is Relation-like Function-like set
X +* (l1 .--> l2) is non empty Relation-like Function-like set
(X +* (l1 .--> l2)) | i1 is Relation-like Function-like set
proj1 X is set
proj1 I is set
(proj1 I) /\ i1 is set
proj1 (X | i1) is set
(proj1 X) /\ i1 is set
proj1 X is set
I is Relation-like Function-like set
X is set
l1 is set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
(I +* (X .--> l1)) . X is set
dom (X .--> l1) is non empty trivial 1 -element Element of bool {X}
bool {X} is non empty set
(X .--> l1) . X is set
I is set
<*I*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
X is set
(<*I*>,1,X) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*X*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
dom <*X*> is non empty trivial 1 -element V92() Element of bool NAT
{1} is non empty trivial 1 -element Element of bool NAT
dom <*I*> is non empty trivial 1 -element V92() Element of bool NAT
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
<*I*> +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
l1 is set
(<*I*>,1,X) . l1 is set
<*X*> . l1 is set
dom (<*I*>,1,X) is V92() Element of bool NAT
dom (1 .--> X) is non empty trivial 1 -element V92() Element of bool {1}
bool {1} is non empty set
(dom <*I*>) \/ (dom (1 .--> X)) is non empty set
{1} \/ {1} is non empty Element of bool NAT
I is Relation-like Function-like set
proj1 I is set
X is set
I . X is set
X .--> (I . X) is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> (I . X) is non empty Relation-like {X} -defined {(I . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(I . X)}:]
{(I . X)} is non empty trivial 1 -element set
[:{X},{(I . X)}:] is non empty Relation-like set
bool [:{X},{(I . X)}:] is non empty set
I +* (X .--> (I . X)) is non empty Relation-like Function-like set
(I,X,(I . X)) is Relation-like Function-like set
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,l1,X) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (I,l1,X) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom (I,l1,X) is V92() Element of bool NAT
dom I is V92() Element of bool NAT
Seg (len (I,l1,X)) is finite len (I,l1,X) -element Element of bool NAT
Seg (len I) is finite len I -element Element of bool NAT
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
I -' 1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is non empty set
l1 is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
dom l1 is V92() Element of bool NAT
l1 | (I -' 1) is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
l1 /^ I is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
l2 is Element of X
(l1,I,l2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*l2*> is non empty trivial Relation-like NAT -defined X -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of X
(l1 | (I -' 1)) ^ <*l2*> is non empty Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
((l1 | (I -' 1)) ^ <*l2*>) ^ (l1 /^ I) is non empty Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of X
len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len (((l1 | (I -' 1)) ^ <*l2*>) ^ (l1 /^ I)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len ((l1 | (I -' 1)) ^ <*l2*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (l1 /^ I) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len ((l1 | (I -' 1)) ^ <*l2*>)) + (len (l1 /^ I)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
len (l1 | (I -' 1)) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
len <*l2*> is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (l1 | (I -' 1))) + (len <*l2*>) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((len (l1 | (I -' 1))) + (len <*l2*>)) + (len (l1 /^ I)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len (l1 | (I -' 1))) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((len (l1 | (I -' 1))) + 1) + (len (l1 /^ I)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I -' 1) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
((I -' 1) + 1) + (len (l1 /^ I)) is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(len l1) - I is ext-real V37() V38() V39() set
((I -' 1) + 1) + ((len l1) - I) is ext-real V37() V38() V39() set
I - 1 is ext-real V37() V38() V39() set
(I - 1) + 1 is ext-real V37() V38() V39() set
((I - 1) + 1) + ((len l1) - I) is ext-real V37() V38() V39() set
len (l1,I,l2) is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(l1,I,l2) . i1 is set
(((l1 | (I -' 1)) ^ <*l2*>) ^ (l1 /^ I)) . i1 is set
I + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(I + 1) - I is ext-real V37() V38() V39() set
i1 - I is ext-real V37() V38() V39() set
i1 -' I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len l1) -' I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom (l1 /^ I) is V92() Element of bool NAT
i1 - (len ((l1 | (I -' 1)) ^ <*l2*>)) is ext-real V37() V38() V39() set
(l1 /^ I) . (i1 - (len ((l1 | (I -' 1)) ^ <*l2*>))) is set
(l1 /^ I) . (i1 -' I) is set
(i1 -' I) + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 . ((i1 -' I) + I) is set
l1 . i1 is set
((l1 | (I -' 1)) ^ <*l2*>) . I is set
i1 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(i1 + 1) - 1 is ext-real V37() V38() V39() set
((l1 | (I -' 1)) ^ <*l2*>) . i1 is set
(l1 | (I -' 1)) . i1 is set
l1 . i1 is set
X is set
I is Relation-like Function-like set
proj1 I is set
l1 is set
I . l1 is set
(I,X,(I . l1)) is Relation-like Function-like set
I . X is set
((I,X,(I . l1)),l1,(I . X)) is Relation-like Function-like set
I is Relation-like Function-like set
X is set
l1 is set
(I,X,l1) is set
proj1 I is set
I . l1 is set
(I,X,(I . l1)) is Relation-like Function-like set
I . X is set
((I,X,(I . l1)),l1,(I . X)) is Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
proj1 I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj1 (I,X,l1) is set
I . l1 is set
(I,X,(I . l1)) is Relation-like Function-like set
I . X is set
((I,X,(I . l1)),l1,(I . X)) is Relation-like Function-like set
proj1 ((I,X,(I . l1)),l1,(I . X)) is set
proj1 (I,X,(I . l1)) is set
I is Relation-like Function-like set
proj2 I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj2 (I,X,l1) is set
{l1} is non empty trivial 1 -element set
(proj2 I) \/ {l1} is non empty set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
proj2 (X .--> l1) is non empty trivial 1 -element set
proj1 I is set
I +* (X .--> l1) is non empty Relation-like Function-like set
proj1 I is set
proj1 I is set
I is Relation-like Function-like set
proj2 I is set
X is set
I . X is set
{(I . X)} is non empty trivial 1 -element set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj2 (I,X,l1) is set
(proj2 (I,X,l1)) \/ {(I . X)} is non empty set
l2 is set
proj1 I is set
i1 is set
I . i1 is set
proj1 (I,X,l1) is set
(I,X,l1) . i1 is set
I is Relation-like Function-like set
proj1 I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj2 (I,X,l1) is set
proj1 (I,X,l1) is set
(I,X,l1) . X is set
I is Relation-like Function-like set
proj2 I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj2 (I,X,l1) is set
proj1 I is set
I . X is set
I . l1 is set
{(I . l1)} is non empty trivial 1 -element set
(proj2 I) \/ {(I . l1)} is non empty set
{(I . X)} is non empty trivial 1 -element set
((proj2 I) \/ {(I . l1)}) \/ {(I . X)} is non empty set
(I,X,(I . l1)) is Relation-like Function-like set
proj2 (I,X,(I . l1)) is set
(proj2 (I,X,(I . l1))) \/ {(I . X)} is non empty set
(I,X,(I . l1)) . l1 is set
((I,X,(I . l1)),l1,(I . X)) is Relation-like Function-like set
proj1 (I,X,(I . l1)) is set
proj1 (I,X,l1) is set
(I,X,l1) . X is set
(I,X,(I . l1)) . X is set
(proj2 (I,X,l1)) \/ {(I . l1)} is non empty set
((proj2 (I,X,l1)) \/ {(I . l1)}) \/ {(I . X)} is non empty set
proj1 I is set
proj1 I is set
F₁() is set
F₂() is non empty set
{ F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() } is set
I is non empty set
{ F₃(b₁) where b₁ is Element of I : b₁ in F₁() } is set
l2 is set
i1 is Element of I
F₃(i1) is set
i1 is Element of F₂()
F₃(i1) is set
l2 is Element of I
i1 is Element of I
F₃(l2) is set
F₃(i1) is set
i2 is Element of F₂()
B is Element of F₂()
the Element of { F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() } is Element of { F₃(b₁) where b₁ is Element of F₂() : b₁ in F₁() }
X is Element of F₂()
F₃(X) is set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
I +* l1 is Relation-like Function-like set
X +* l1 is Relation-like Function-like set
l2 is set
proj1 (I +* l1) is set
(proj1 (I +* l1)) \ l2 is Element of bool (proj1 (I +* l1))
bool (proj1 (I +* l1)) is non empty set
(I +* l1) | ((proj1 (I +* l1)) \ l2) is Relation-like Function-like set
proj1 ((I +* l1) | ((proj1 (I +* l1)) \ l2)) is set
proj1 I is set
proj1 l1 is set
(proj1 I) \/ (proj1 l1) is set
((proj1 I) \/ (proj1 l1)) \ l2 is Element of bool ((proj1 I) \/ (proj1 l1))
bool ((proj1 I) \/ (proj1 l1)) is non empty set
(proj1 I) \ l2 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
(proj1 l1) \ l2 is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
((proj1 I) \ l2) \/ ((proj1 l1) \ l2) is set
I | ((proj1 I) \ l2) is Relation-like Function-like set
proj1 X is set
(proj1 X) \ l2 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
X | ((proj1 X) \ l2) is Relation-like Function-like set
proj1 (X | ((proj1 X) \ l2)) is set
(proj1 X) \/ (proj1 l1) is set
((proj1 X) \/ (proj1 l1)) \ l2 is Element of bool ((proj1 X) \/ (proj1 l1))
bool ((proj1 X) \/ (proj1 l1)) is non empty set
proj1 (X +* l1) is set
(proj1 (X +* l1)) \ l2 is Element of bool (proj1 (X +* l1))
bool (proj1 (X +* l1)) is non empty set
(X +* l1) | ((proj1 (X +* l1)) \ l2) is Relation-like Function-like set
proj1 ((X +* l1) | ((proj1 (X +* l1)) \ l2)) is set
i1 is set
((I +* l1) | ((proj1 (I +* l1)) \ l2)) . i1 is set
(I +* l1) . i1 is set
l1 . i1 is set
(X +* l1) . i1 is set
((X +* l1) | ((proj1 (X +* l1)) \ l2)) . i1 is set
((I +* l1) | ((proj1 (I +* l1)) \ l2)) . i1 is set
(I +* l1) . i1 is set
I . i1 is set
(X | ((proj1 X) \ l2)) . i1 is set
X . i1 is set
(X +* l1) . i1 is set
((X +* l1) | ((proj1 (X +* l1)) \ l2)) . i1 is set
I is Relation-like Function-like set
X is Relation-like Function-like set
l1 is Relation-like Function-like set
l1 +* I is Relation-like Function-like set
l1 +* X is Relation-like Function-like set
l2 is set
proj1 I is set
(proj1 I) \ l2 is Element of bool (proj1 I)
bool (proj1 I) is non empty set
I | ((proj1 I) \ l2) is Relation-like Function-like set
proj1 X is set
(proj1 X) \ l2 is Element of bool (proj1 X)
bool (proj1 X) is non empty set
X | ((proj1 X) \ l2) is Relation-like Function-like set
proj1 (X | ((proj1 X) \ l2)) is set
proj1 (l1 +* I) is set
(proj1 (l1 +* I)) \ l2 is Element of bool (proj1 (l1 +* I))
bool (proj1 (l1 +* I)) is non empty set
(l1 +* I) | ((proj1 (l1 +* I)) \ l2) is Relation-like Function-like set
proj1 ((l1 +* I) | ((proj1 (l1 +* I)) \ l2)) is set
proj1 l1 is set
(proj1 l1) \/ (proj1 I) is set
((proj1 l1) \/ (proj1 I)) \ l2 is Element of bool ((proj1 l1) \/ (proj1 I))
bool ((proj1 l1) \/ (proj1 I)) is non empty set
(proj1 l1) \ l2 is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
((proj1 l1) \ l2) \/ ((proj1 I) \ l2) is set
(proj1 l1) \/ (proj1 X) is set
((proj1 l1) \/ (proj1 X)) \ l2 is Element of bool ((proj1 l1) \/ (proj1 X))
bool ((proj1 l1) \/ (proj1 X)) is non empty set
proj1 (l1 +* X) is set
(proj1 (l1 +* X)) \ l2 is Element of bool (proj1 (l1 +* X))
bool (proj1 (l1 +* X)) is non empty set
(l1 +* X) | ((proj1 (l1 +* X)) \ l2) is Relation-like Function-like set
proj1 ((l1 +* X) | ((proj1 (l1 +* X)) \ l2)) is set
i1 is set
((l1 +* I) | ((proj1 (l1 +* I)) \ l2)) . i1 is set
(l1 +* I) . i1 is set
I . i1 is set
(X | ((proj1 X) \ l2)) . i1 is set
X . i1 is set
(l1 +* X) . i1 is set
((l1 +* X) | ((proj1 (l1 +* X)) \ l2)) . i1 is set
((l1 +* I) | ((proj1 (l1 +* I)) \ l2)) . i1 is set
(l1 +* I) . i1 is set
l1 . i1 is set
(l1 +* X) . i1 is set
((l1 +* X) | ((proj1 (l1 +* X)) \ l2)) . i1 is set
I is Relation-like Function-like set
l1 is Relation-like Function-like set
I +* l1 is Relation-like Function-like set
X is Relation-like Function-like set
X +* l1 is Relation-like Function-like set
proj1 l1 is set
proj1 I is set
(proj1 I) \ (proj1 l1) is Element of bool (proj1 I)
bool (proj1 I) is non empty set
proj1 X is set
(proj1 X) \ (proj1 l1) is Element of bool (proj1 X)
bool (proj1 X) is non empty set
proj1 (I +* l1) is set
l2 is set
(I +* l1) . l2 is set
(X +* l1) . l2 is set
l1 . l2 is set
(proj1 I) \/ (proj1 l1) is set
I | ((proj1 I) \ (proj1 l1)) is Relation-like Function-like set
X | ((proj1 X) \ (proj1 l1)) is Relation-like Function-like set
I . l2 is set
(X | ((proj1 X) \ (proj1 l1))) . l2 is set
X . l2 is set
(proj1 I) \/ (proj1 l1) is set
((proj1 X) \ (proj1 l1)) \/ (proj1 l1) is set
(proj1 X) \/ (proj1 l1) is set
proj1 (X +* l1) is set
I is set
X is set
l1 is set
l2 is Relation-like Function-like set
l2 . I is set
l2 . X is set
l2 . l1 is set
proj1 l2 is set
id (proj1 l2) is Relation-like proj1 l2 -defined proj1 l2 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 l2),(proj1 l2):]
[:(proj1 l2),(proj1 l2):] is Relation-like set
bool [:(proj1 l2),(proj1 l2):] is non empty set
((id (proj1 l2)),I,X) is Relation-like Function-like set
((id (proj1 l2)),I,X) (#) l2 is Relation-like Function-like set
(((id (proj1 l2)),I,X) (#) l2) . l1 is set
dom (id (proj1 l2)) is Element of bool (proj1 l2)
bool (proj1 l2) is non empty set
proj1 ((id (proj1 l2)),I,X) is set
((id (proj1 l2)),I,X) . I is set
((id (proj1 l2)),I,X) . l1 is set
(id (proj1 l2)) . l1 is set
proj1 (((id (proj1 l2)),I,X) (#) l2) is set
I is set
X is set
l1 is Relation-like Function-like set
proj1 l1 is set
l1 . I is set
l1 . X is set
id (proj1 l1) is Relation-like proj1 l1 -defined proj1 l1 -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 l1),(proj1 l1):]
[:(proj1 l1),(proj1 l1):] is Relation-like set
bool [:(proj1 l1),(proj1 l1):] is non empty set
((id (proj1 l1)),I,X) is Relation-like Function-like set
((id (proj1 l1)),I,X) (#) l1 is Relation-like Function-like set
dom (id (proj1 l1)) is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
proj1 ((id (proj1 l1)),I,X) is set
proj2 ((id (proj1 l1)),I,X) is set
i2 is set
B is set
((id (proj1 l1)),I,X) . B is set
(id (proj1 l1)) . B is set
proj1 (((id (proj1 l1)),I,X) (#) l1) is set
i2 is set
l1 . i2 is set
(((id (proj1 l1)),I,X) (#) l1) . i2 is set
I is Relation-like Function-like set
proj1 I is set
X is set
I . X is set
X .--> (I . X) is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> (I . X) is non empty Relation-like {X} -defined {(I . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(I . X)}:]
{(I . X)} is non empty trivial 1 -element set
[:{X},{(I . X)}:] is non empty Relation-like set
bool [:{X},{(I . X)}:] is non empty set
I +* (X .--> (I . X)) is non empty Relation-like Function-like set
(I,X,(I . X)) is Relation-like Function-like set
I is set
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:I,I:]
l1 is Element of I
l2 is Element of I
X . l2 is set
(X,l1,(X . l2)) is Relation-like Function-like set
X . l1 is set
((X,l1,(X . l2)),l2,(X . l1)) is Relation-like Function-like set
proj1 ((X,l1,(X . l2)),l2,(X . l1)) is set
proj1 (X,l1,(X . l2)) is set
dom X is Element of bool I
bool I is non empty set
rng X is Element of bool I
((X,l1,(X . l2)),l2,(X . l1)) . l1 is set
(X,l1,(X . l2)) . l1 is set
B is set
((X,l1,(X . l2)),l2,(X . l1)) . B is set
(X,l1,(X . l2)) . B is set
X . B is set
((X,l1,(X . l2)),l2,(X . l1)) . l2 is set
B is set
proj2 ((X,l1,(X . l2)),l2,(X . l1)) is set
B is set
((X,l1,(X . l2)),l2,(X . l1)) . B is set
X . B is set
B is set
X . B is set
((X,l1,(X . l2)),l2,(X . l1)) . B is set
B is set
e is set
B is Relation-like I -defined I -valued Function-like total quasi_total Element of bool [:I,I:]
B . B is set
B . e is set
X . e is set
X . B is set
X . e is set
X . B is set
X . B is set
X . e is set
rng B is Element of bool I
I is Relation-like Function-like set
proj1 I is set
[:(proj1 I),(proj1 I):] is Relation-like set
bool [:(proj1 I),(proj1 I):] is non empty set
X is set
l1 is set
I . l1 is set
(I,X,(I . l1)) is Relation-like Function-like set
I . X is set
((I,X,(I . l1)),l1,(I . X)) is Relation-like Function-like set
id (proj1 I) is Relation-like proj1 I -defined proj1 I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:(proj1 I),(proj1 I):]
(id (proj1 I)) . X is set
(id (proj1 I)) . l1 is set
((id (proj1 I)),X,l1) is Relation-like Function-like set
(((id (proj1 I)),X,l1),l1,X) is Relation-like Function-like set
i1 is Relation-like proj1 I -defined proj1 I -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 I),(proj1 I):]
i1 (#) I is Relation-like proj1 I -defined Function-like set
dom (id (proj1 I)) is Element of bool (proj1 I)
bool (proj1 I) is non empty set
proj1 (I,X,(I . l1)) is set
proj1 ((I,X,(I . l1)),l1,(I . X)) is set
dom i1 is Element of bool (proj1 I)
proj1 ((id (proj1 I)),X,l1) is set
rng i1 is Element of bool (proj1 I)
dom (i1 (#) I) is Element of bool (proj1 I)
l is set
((I,X,(I . l1)),l1,(I . X)) . l is set
(i1 (#) I) . l is set
(I,X,(I . l1)) . l is set
((id (proj1 I)),X,l1) . X is set
I . (((id (proj1 I)),X,l1) . X) is set
i1 . X is set
I . (i1 . X) is set
i1 . l1 is set
I . (i1 . l1) is set
i1 . l is set
((id (proj1 I)),X,l1) . l is set
(id (proj1 I)) . l is set
(I,X,(I . l1)) . l is set
I . (i1 . l) is set
((id (proj1 I)),X,((id (proj1 I)) . l1)) is Relation-like Function-like set
((I,X,(I . l1)),l1,(I . X)) . l is set
(i1 (#) I) . l is set
I is Relation-like Function-like set
proj1 I is set
X is set
l1 is set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
proj1 (I +* (X .--> l1)) is non empty set
(I,X,l1) is Relation-like Function-like set
proj1 (I,X,l1) is set
I is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
dom I is V92() Element of bool NAT
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I /. l2 is ext-real V37() V38() V39() Element of INT
(INT,I,l1,(I /. l2)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
I /. l1 is ext-real V37() V38() V39() Element of INT
(INT,(INT,I,l1,(I /. l2)),l2,(I /. l1)) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
I . l1 is set
X . l2 is set
I . l2 is set
X . l1 is set
dom (INT,I,l1,(I /. l2)) is V92() Element of bool NAT
(INT,I,l1,(I /. l2)) . l1 is set
i1 is set
X . i1 is set
(INT,I,l1,(I /. l2)) . i1 is set
I . i1 is set
dom X is V92() Element of bool NAT
i1 is set
I . i1 is set
X . i1 is set
I is Relation-like Function-like set
X is set
l2 is set
i2 is set
l1 is set
X .--> l1 is non empty trivial Relation-like {X} -defined Function-like one-to-one constant 1 -element set
{X} is non empty trivial 1 -element set
{X} --> l1 is non empty Relation-like {X} -defined {l1} -valued Function-like constant total quasi_total Element of bool [:{X},{l1}:]
{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set
i1 is set
l2 .--> i1 is non empty trivial Relation-like {l2} -defined Function-like one-to-one constant 1 -element set
{l2} is non empty trivial 1 -element set
{l2} --> i1 is non empty Relation-like {l2} -defined {i1} -valued Function-like constant total quasi_total Element of bool [:{l2},{i1}:]
{i1} is non empty trivial 1 -element set
[:{l2},{i1}:] is non empty Relation-like set
bool [:{l2},{i1}:] is non empty set
(I +* (X .--> l1)) +* (l2 .--> i1) is non empty Relation-like Function-like set
B is set
i2 .--> B is non empty trivial Relation-like {i2} -defined Function-like one-to-one constant 1 -element set
{i2} is non empty trivial 1 -element set
{i2} --> B is non empty Relation-like {i2} -defined {B} -valued Function-like constant total quasi_total Element of bool [:{i2},{B}:]
{B} is non empty trivial 1 -element set
[:{i2},{B}:] is non empty Relation-like set
bool [:{i2},{B}:] is non empty set
((I +* (X .--> l1)) +* (l2 .--> i1)) +* (i2 .--> B) is non empty Relation-like Function-like set
(((I +* (X .--> l1)) +* (l2 .--> i1)) +* (i2 .--> B)) . X is set
(I +* (X .--> l1)) . X is set
I is set
X is set
[:I,X:] is Relation-like set
bool [:I,X:] is non empty set
l2 is set
l1 is set
i1 is Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:]
(i1,l1,l2) is Relation-like Function-like set
dom i1 is Element of bool I
bool I is non empty set
l1 .--> l2 is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
{l2} is non empty trivial 1 -element set
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
i1 +* (l1 .--> l2) is non empty Relation-like Function-like set
proj2 (l1 .--> l2) is non empty trivial 1 -element set
proj2 (i1 +* (l1 .--> l2)) is non empty set
rng i1 is Element of bool X
bool X is non empty set
(rng i1) \/ (proj2 (l1 .--> l2)) is non empty set
X \/ X is set
proj1 (i1 +* (l1 .--> l2)) is non empty set
dom (l1 .--> l2) is non empty trivial 1 -element Element of bool {l1}
bool {l1} is non empty set
I \/ (dom (l1 .--> l2)) is non empty set
I \/ {l1} is non empty set
I is set
id I is Relation-like I -defined I -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:I,I:]
[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
X is Relation-like Function-like set
proj2 X is set
l1 is set
l2 is set
X +~ (l1,l2) is Relation-like Function-like set
l1 .--> l2 is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
{l2} is non empty trivial 1 -element set
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
X (#) (l1 .--> l2) is Relation-like Function-like set
X +* (X (#) (l1 .--> l2)) is Relation-like Function-like set
((id I),l1,l2) is Relation-like Function-like set
X (#) ((id I),l1,l2) is Relation-like Function-like set
dom (id I) is Element of bool I
bool I is non empty set
X (#) (id I) is Relation-like I -valued Function-like set
(X (#) (id I)) +* (X (#) (l1 .--> l2)) is Relation-like Function-like set
(id I) +* (l1 .--> l2) is non empty Relation-like Function-like set
X (#) ((id I) +* (l1 .--> l2)) is Relation-like Function-like set
dom (id I) is Element of bool I
bool I is non empty set
X (#) (id I) is Relation-like I -valued Function-like set
I is Relation-like Function-like set
X is Relation-like Function-like set
I +* X is Relation-like Function-like set
l1 is set
l2 is set
(I +* X) +~ (l1,l2) is Relation-like Function-like set
l1 .--> l2 is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
{l2} is non empty trivial 1 -element set
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
(I +* X) (#) (l1 .--> l2) is Relation-like Function-like set
(I +* X) +* ((I +* X) (#) (l1 .--> l2)) is Relation-like Function-like set
I +~ (l1,l2) is Relation-like Function-like set
I (#) (l1 .--> l2) is Relation-like Function-like set
I +* (I (#) (l1 .--> l2)) is Relation-like Function-like set
X +~ (l1,l2) is Relation-like Function-like set
X (#) (l1 .--> l2) is Relation-like Function-like set
X +* (X (#) (l1 .--> l2)) is Relation-like Function-like set
(I +~ (l1,l2)) +* (X +~ (l1,l2)) is Relation-like Function-like set
proj2 I is set
proj2 X is set
(proj2 I) \/ (proj2 X) is set
id ((proj2 I) \/ (proj2 X)) is Relation-like (proj2 I) \/ (proj2 X) -defined (proj2 I) \/ (proj2 X) -valued Function-like one-to-one total quasi_total onto bijective V66() V68() V69() V73() Element of bool [:((proj2 I) \/ (proj2 X)),((proj2 I) \/ (proj2 X)):]
[:((proj2 I) \/ (proj2 X)),((proj2 I) \/ (proj2 X)):] is Relation-like set
bool [:((proj2 I) \/ (proj2 X)),((proj2 I) \/ (proj2 X)):] is non empty set
((id ((proj2 I) \/ (proj2 X))),l1,l2) is Relation-like Function-like set
X (#) ((id ((proj2 I) \/ (proj2 X))),l1,l2) is Relation-like Function-like set
proj1 ((id ((proj2 I) \/ (proj2 X))),l1,l2) is set
dom (id ((proj2 I) \/ (proj2 X))) is Element of bool ((proj2 I) \/ (proj2 X))
bool ((proj2 I) \/ (proj2 X)) is non empty set
proj2 (I +* X) is set
(I +* X) (#) ((id ((proj2 I) \/ (proj2 X))),l1,l2) is Relation-like Function-like set
I (#) ((id ((proj2 I) \/ (proj2 X))),l1,l2) is Relation-like Function-like set
(I (#) ((id ((proj2 I) \/ (proj2 X))),l1,l2)) +* (X (#) ((id ((proj2 I) \/ (proj2 X))),l1,l2)) is Relation-like Function-like set
X is set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
I is set
((NAT --> X),0,I) is Relation-like Function-like set
I is set
X is set
(I,X) is set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
((NAT --> X),0,I) is Relation-like Function-like set
I is set
X is set
(I,X) is Relation-like Function-like set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
((NAT --> X),0,I) is Relation-like Function-like set
proj1 (I,X) is set
proj1 ((NAT --> X),0,I) is set
dom (NAT --> X) is non empty V18() V19() V20() V92() Element of bool NAT
I is non empty set
X is Element of I
l1 is Element of I
(X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined I -valued {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
((NAT --> l1),0,X) is Relation-like Function-like set
[:NAT,I:] is non empty Relation-like non finite set
bool [:NAT,I:] is non empty non finite set
NAT --> l1 is non empty Relation-like NAT -defined I -valued Function-like constant total V22() quasi_total Element of bool [:NAT,I:]
((NAT --> l1),0,X) is Relation-like Function-like set
I is set
X is set
(I,X) is Relation-like Function-like set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
((NAT --> X),0,I) is Relation-like Function-like set
(I,X) . 0 is set
dom (NAT --> X) is non empty V18() V19() V20() V92() Element of bool NAT
I is set
X is set
(I,X) is Relation-like Function-like set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
((NAT --> X),0,I) is Relation-like Function-like set
l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,X) . l1 is set
(NAT --> X) . l1 is set
l1 is set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
I is set
X is set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} is non empty trivial functional 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
I is set
X is set
l1 is set
(I,X,l1) is set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
proj1 (I,X,l1) is set
dom (NAT --> l1) is non empty V18() V19() V20() V92() Element of bool NAT
dom ((0,1) --> (I,X)) is non empty V92() Element of bool NAT
(dom (NAT --> l1)) \/ (dom ((0,1) --> (I,X))) is non empty Element of bool NAT
NAT \/ (dom ((0,1) --> (I,X))) is non empty set
{0,1} is non empty Element of bool NAT
NAT \/ {0,1} is non empty set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
(I,X,l1) . 0 is set
dom ((0,1) --> (I,X)) is non empty V92() Element of bool NAT
{0,1} is non empty Element of bool NAT
((NAT --> l1) +* ((0,1) --> (I,X))) . 0 is set
((0,1) --> (I,X)) . 0 is set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
(I,X,l1) . 1 is set
dom ((0,1) --> (I,X)) is non empty V92() Element of bool NAT
{0,1} is non empty Element of bool NAT
((NAT --> l1) +* ((0,1) --> (I,X))) . 1 is set
((0,1) --> (I,X)) . 1 is set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
l2 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,X,l1) . l2 is set
dom ((0,1) --> (I,X)) is non empty V92() Element of bool NAT
{0,1} is non empty Element of bool NAT
((NAT --> l1) +* ((0,1) --> (I,X))) . l2 is set
(NAT --> l1) . l2 is set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
(I,l1) is Relation-like Function-like set
((NAT --> l1),0,I) is Relation-like Function-like set
((I,l1),1,X) is Relation-like Function-like set
proj1 (I,l1) is set
proj1 (I,X,l1) is set
proj1 ((I,l1),1,X) is set
i2 is set
(I,X,l1) . i2 is set
((I,l1),1,X) . i2 is set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,l1) . i2 is set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
(I,l1) . i2 is set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal set
I is non empty set
X is Element of I
l1 is Element of I
l2 is Element of I
(X,l1,l2) is Relation-like Function-like set
NAT --> l2 is non empty Relation-like NAT -defined I -valued {l2} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l2}:]
{l2} is non empty trivial 1 -element set
[:NAT,{l2}:] is non empty Relation-like non finite set
bool [:NAT,{l2}:] is non empty non finite set
(0,1) --> (X,l1) is non empty Relation-like NAT -defined Function-like set
0 .--> X is non empty trivial Relation-like NAT -defined {0} -defined I -valued Function-like one-to-one constant 1 -element set
{0} --> X is non empty Relation-like {0} -defined I -valued {X} -valued Function-like constant total quasi_total Element of bool [:{0},{X}:]
{X} is non empty trivial 1 -element set
[:{0},{X}:] is non empty Relation-like set
bool [:{0},{X}:] is non empty set
1 .--> l1 is non empty trivial Relation-like NAT -defined {1} -defined I -valued Function-like one-to-one constant 1 -element set
{1} --> l1 is non empty Relation-like {1} -defined I -valued {l1} -valued Function-like constant total quasi_total Element of bool [:{1},{l1}:]
{l1} is non empty trivial 1 -element set
[:{1},{l1}:] is non empty Relation-like set
bool [:{1},{l1}:] is non empty set
(0 .--> X) +* (1 .--> l1) is non empty Relation-like NAT -defined I -valued Function-like set
(NAT --> l2) +* ((0,1) --> (X,l1)) is non empty Relation-like NAT -defined Function-like total set
[:NAT,I:] is non empty Relation-like non finite set
bool [:NAT,I:] is non empty non finite set
(I,X,l2) is non empty Relation-like NAT -defined I -valued Function-like total quasi_total Element of bool [:NAT,I:]
((NAT --> l2),0,X) is Relation-like Function-like set
((I,X,l2),1,l1) is Relation-like Function-like set
I is set
X is set
(I,X) is Relation-like Function-like set
NAT --> X is non empty Relation-like NAT -defined {X} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{X}:]
{X} is non empty trivial 1 -element set
[:NAT,{X}:] is non empty Relation-like non finite set
bool [:NAT,{X}:] is non empty non finite set
((NAT --> X),0,I) is Relation-like Function-like set
proj2 (I,X) is set
{I,X} is non empty set
rng (NAT --> X) is non empty trivial 1 -element Element of bool {X}
bool {X} is non empty set
proj2 ((NAT --> X),0,I) is set
{I} is non empty trivial 1 -element set
{X} \/ {I} is non empty set
l1 is set
dom (NAT --> X) is non empty V18() V19() V20() V92() Element of bool NAT
proj1 (I,X) is set
(I,X) . 1 is set
I is set
X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
NAT --> l1 is non empty Relation-like NAT -defined {l1} -valued Function-like constant total V22() quasi_total Element of bool [:NAT,{l1}:]
{l1} is non empty trivial 1 -element set
[:NAT,{l1}:] is non empty Relation-like non finite set
bool [:NAT,{l1}:] is non empty non finite set
(0,1) --> (I,X) is non empty Relation-like NAT -defined Function-like set
0 .--> I is non empty trivial Relation-like NAT -defined {0} -defined Function-like one-to-one constant 1 -element set
{0} --> I is non empty Relation-like {0} -defined {I} -valued Function-like constant total quasi_total Element of bool [:{0},{I}:]
{I} is non empty trivial 1 -element set
[:{0},{I}:] is non empty Relation-like set
bool [:{0},{I}:] is non empty set
1 .--> X is non empty trivial Relation-like NAT -defined {1} -defined Function-like one-to-one constant 1 -element set
{1} --> X is non empty Relation-like {1} -defined {X} -valued Function-like constant total quasi_total Element of bool [:{1},{X}:]
{X} is non empty trivial 1 -element set
[:{1},{X}:] is non empty Relation-like set
bool [:{1},{X}:] is non empty set
(0 .--> I) +* (1 .--> X) is non empty Relation-like NAT -defined Function-like set
(NAT --> l1) +* ((0,1) --> (I,X)) is non empty Relation-like NAT -defined Function-like total set
proj2 (I,X,l1) is set
{I,X,l1} is non empty set
(I,l1) is Relation-like Function-like set
((NAT --> l1),0,I) is Relation-like Function-like set
((I,l1),1,X) is Relation-like Function-like set
proj1 (I,X,l1) is set
proj1 (I,l1) is set
dom (NAT --> l1) is non empty V18() V19() V20() V92() Element of bool NAT
(I,X,l1) . 2 is set
(I,X,l1) . 1 is set
proj2 (I,l1) is set
{I,l1} is non empty set
proj2 ((I,l1),1,X) is set
{I,l1} \/ {X} is non empty set
{I,l1,X} is non empty set
l2 is set
(I,X,l1) . 0 is set
I is set
X is set
[:I,X:] is Relation-like set
bool [:I,X:] is non empty set
l1 is Relation-like I -defined X -valued Function-like quasi_total Element of bool [:I,X:]
l2 is set
i1 is Element of X
(l1,l2,i1) is Relation-like Function-like set
proj2 (l1,l2,i1) is set
rng l1 is Element of bool X
bool X is non empty set
{i1} is non empty trivial 1 -element set
(rng l1) \/ {i1} is non empty set
dom l1 is Element of bool I
bool I is non empty set
dom l1 is Element of bool I
bool I is non empty set
proj1 (l1,l2,i1) is set
I is non empty set
X is non empty set
[:I,X:] is non empty Relation-like set
bool [:I,X:] is non empty set
l1 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l2 is Element of I
i1 is set
(l1,l2,i1) is Relation-like Function-like set
(l1,l2,i1) . l2 is set
dom l1 is non empty Element of bool I
bool I is non empty set
I is non empty set
X is non empty set
[:I,X:] is non empty Relation-like set
bool [:I,X:] is non empty set
l1 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
l2 is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
i1 is Element of I
l1 . i1 is Element of X
(I,X,l2,i1,(l1 . i1)) is non empty Relation-like I -defined X -valued Function-like total quasi_total Element of bool [:I,X:]
dom l2 is non empty Element of bool I
bool I is non empty set
dom l1 is non empty Element of bool I
{i1} is non empty trivial 1 -element Element of bool I
I \/ {i1} is non empty set
(dom l2) \/ {i1} is non empty Element of bool I
i1 .--> (l1 . i1) is non empty trivial Relation-like I -defined {i1} -defined X -valued Function-like one-to-one constant 1 -element set
{i1} is non empty trivial 1 -element set
{i1} --> (l1 . i1) is non empty Relation-like {i1} -defined X -valued {(l1 . i1)} -valued Function-like constant total quasi_total Element of bool [:{i1},{(l1 . i1)}:]
{(l1 . i1)} is non empty trivial 1 -element set
[:{i1},{(l1 . i1)}:] is non empty Relation-like set
bool [:{i1},{(l1 . i1)}:] is non empty set
dom (i1 .--> (l1 . i1)) is non empty trivial 1 -element Element of bool I
(dom l2) \/ (dom (i1 .--> (l1 . i1))) is non empty Element of bool I
i2 is set
l1 . i2 is set
(i1 .--> (l1 . i1)) . i2 is set
l2 . i2 is set
l2 +* (i1 .--> (l1 . i1)) is non empty Relation-like I -defined X -valued Function-like total set
I is set
X is Relation-like Function-like set
l1 is Relation-like I -defined Function-like set
X +* l1 is Relation-like Function-like set
dom l1 is Element of bool I
bool I is non empty set
I is set
X is Relation-like I -defined Function-like set
l1 is Relation-like I -defined Function-like set
dom l1 is Element of bool I
bool I is non empty set
(dom l1) \ I is Element of bool I
dom X is Element of bool I
(dom X) \ I is Element of bool I
X | ((dom X) \ I) is Relation-like (dom X) \ I -defined I -defined Function-like set
l1 | ((dom l1) \ I) is Relation-like (dom l1) \ I -defined I -defined Function-like set
I is set
X is Relation-like I -defined Function-like set
l1 is Relation-like I -defined Function-like set
l2 is Relation-like Function-like set
l2 +* X is Relation-like Function-like set
l2 +* l1 is Relation-like Function-like set
I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X is Relation-like NAT -defined Function-like set
Shift (X,I) is Relation-like NAT -defined Function-like set
card (Shift (X,I)) is V18() V19() V20() cardinal set
card X is V18() V19() V20() cardinal set
dom X is V92() Element of bool NAT
l1 is set
{ b₁ where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : H₁(b₁) in dom X } is set
{ b₁ where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : S₂[b₁] } is set
{ H₂(b₁) where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : ( b₁ in { b₁ where b₂ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : S₂[b₁] } & S₁[b₁] ) } is set
{ H₂(b₁) where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : b₁ in { b₁ where b₂ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : H₁(b₁) in dom X } } is set
{ (b₁ + I) where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : b₁ in dom X } is set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B is set
B is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
B + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
e is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
{ b₁ where b₁ is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : b₁ in dom X } is set
e is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
e + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
e is set
l is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
dom (Shift (X,I)) is V92() Element of bool NAT
e is set
l is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l + I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
card (dom (Shift (X,I))) is V18() V19() V20() cardinal set
card (dom X) is V18() V19() V20() cardinal set
I is set
X is set
I \/ X is set
l1 is Relation-like Function-like set
proj1 l1 is set
l1 | X is Relation-like Function-like set
l2 is Relation-like Function-like set
proj1 l2 is set
l2 | X is Relation-like Function-like set
(proj1 l1) \ I is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
l1 | ((proj1 l1) \ I) is Relation-like Function-like set
(proj1 l2) \ I is Element of bool (proj1 l2)
bool (proj1 l2) is non empty set
l2 | ((proj1 l2) \ I) is Relation-like Function-like set
I is set
X is set
l1 is Relation-like Function-like set
proj1 l1 is set
l1 | I is Relation-like Function-like set
l2 is Relation-like Function-like set
proj1 l2 is set
l2 | I is Relation-like Function-like set
(proj1 l1) \ X is Element of bool (proj1 l1)
bool (proj1 l1) is non empty set
l1 | ((proj1 l1) \ X) is Relation-like Function-like set
(proj1 l2) \ X is Element of bool (proj1 l2)
bool (proj1 l2) is non empty set
l2 | ((proj1 l2) \ X) is Relation-like Function-like set
I is set
X is set
l1 is set
X \/ l1 is set
l2 is Relation-like I -defined Function-like total set
l2 | l1 is Relation-like l1 -defined I -defined Function-like set
i1 is Relation-like I -defined Function-like total set
i1 | l1 is Relation-like l1 -defined I -defined Function-like set
dom l2 is Element of bool I
bool I is non empty set
dom i1 is Element of bool I
I is set
X is set
l1 is set
l2 is Relation-like X -defined Function-like total set
l2 | I is Relation-like I -defined X -defined Function-like set
i1 is Relation-like X -defined Function-like total set
i1 | I is Relation-like I -defined X -defined Function-like set
dom l2 is Element of bool X
bool X is non empty set
dom i1 is Element of bool X
I is non empty set
X is Relation-like I -valued Function-like set
l1 is set
l2 is Element of I
(X,l1,l2) is Relation-like Function-like set
proj2 (X,l1,l2) is set
rng X is Element of bool I
bool I is non empty set
{l2} is non empty trivial 1 -element Element of bool I
(rng X) \/ {l2} is non empty Element of bool I
I is Relation-like Function-like set
proj1 I is set
X is Relation-like Function-like set
l1 is set
l2 is set
(X,l1,l2) is Relation-like Function-like set
l1 .--> l2 is non empty trivial Relation-like {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> l2 is non empty Relation-like {l1} -defined {l2} -valued Function-like constant total quasi_total Element of bool [:{l1},{l2}:]
{l2} is non empty trivial 1 -element set
[:{l1},{l2}:] is non empty Relation-like set
bool [:{l1},{l2}:] is non empty set
I +* (l1 .--> l2) is non empty Relation-like Function-like set
proj1 X is set
X +* (l1 .--> l2) is non empty Relation-like Function-like set
proj1 X is set
proj1 X is set
I is non empty set
X is Relation-like I -defined Function-like total set
l1 is Element of I
l2 is Element of I
i1 is set
i2 is set
(l1,l2) --> (i1,i2) is non empty Relation-like I -defined Function-like set
l1 .--> i1 is non empty trivial Relation-like I -defined {l1} -defined Function-like one-to-one constant 1 -element set
{l1} is non empty trivial 1 -element set
{l1} --> i1 is non empty Relation-like {l1} -defined {i1} -valued Function-like constant total quasi_total Element of bool [:{l1},{i1}:]
{i1} is non empty trivial 1 -element set
[:{l1},{i1}:] is non empty Relation-like set
bool [:{l1},{i1}:] is non empty set
l2 .--> i2 is non empty trivial Relation-like I -defined {l2} -defined Function-like one-to-one constant 1 -element set
{l2} is non empty trivial 1 -element set
{l2} --> i2 is non empty Relation-like {l2} -defined {i2} -valued Function-like constant total quasi_total Element of bool [:{l2},{i2}:]
{i2} is non empty trivial 1 -element set
[:{l2},{i2}:] is non empty Relation-like set
bool [:{l2},{i2}:] is non empty set
(l1 .--> i1) +* (l2 .--> i2) is non empty Relation-like I -defined Function-like set
X +* ((l1,l2) --> (i1,i2)) is non empty Relation-like I -defined Function-like total set
(X,l1,i1) is Relation-like Function-like set
((X,l1,i1),l2,i2) is Relation-like Function-like set
dom X is Element of bool I
bool I is non empty set
proj1 (X,l1,i1) is set
X +* ((l1 .--> i1) +* (l2 .--> i2)) is non empty Relation-like I -defined Function-like total set
X +* (l1 .--> i1) is non empty Relation-like I -defined Function-like total set
(X +* (l1 .--> i1)) +* (l2 .--> i2) is non empty Relation-like I -defined Function-like total set
(X,l1,i1) +* (l2 .--> i2) is non empty Relation-like Function-like set