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
{ b1 where b1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT : not l1 + 1 <= b1 } 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
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2():] is non empty Relation-like set
[:[:F1(),F2():],F3():] is non empty Relation-like set
bool [:[:F1(),F2():],F3():] is non empty set
I is Element of [:F1(),F2():]
I `1 is Element of F1()
I `2 is Element of F2()
F4((I `1),(I `2)) is set
I is non empty Relation-like [:F1(),F2():] -defined F3() -valued Function-like total quasi_total Element of bool [:[:F1(),F2():],F3():]
X is Element of F1()
l1 is Element of F2()
I . (X,l1) is Element of F3()
[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
F4(X,l1) is set
[X,l1] is V25() Element of [:F1(),F2():]
[X,l1] `1 is Element of F1()
[X,l1] `2 is Element of F2()
F1() is set
F2() is non empty set
{ F3(b1) where b1 is Element of F2() : F4(b1) in F1() } is set
the Element of { F3(b1) where b1 is Element of F2() : F4(b1) in F1() } is Element of { F3(b1) where b1 is Element of F2() : F4(b1) in F1() }
X is Element of F2()
F3(X) is set
F4(X) is set
I is non empty set
{ b1 where b1 is Element of F2() : F4(b1) in I } is set
{ b1 where b1 is Element of I : S1[b1] } is set
{ F3(b1) where b1 is Element of F2() : b1 in { b1 where b2 is Element of F2() : F4(b1) in I } } is set
l2 is set
i1 is Element of F2()
F3(i1) is set
F4(i1) is set
l2 is set
i1 is Element of F2()
F3(i1) is set
i2 is Element of F2()
F4(i2) is set
{ [F4(b1),b1] where b1 is Element of F2() : verum } is set
l2 is set
i1 is set
i2 is Element of I
B is Element of F2()
F4(B) is set
B is Element of F2()
F4(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 F2()
F4(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 F2()
F4(e) is set
[F4(e),e] is V25() set
{F4(e),e} is non empty set
{F4(e)} is non empty trivial 1 -element set
{{F4(e),e},{F4(e)}} is non empty set
l is Element of F2()
F4(l) is set
[F4(l),l] is V25() set
{F4(l),l} is non empty set
{F4(l)} is non empty trivial 1 -element set
{{F4(l),l},{F4(l)}} is non empty set
bool I is non empty set
F1() is set
F2() is non empty set
{ b1 where b1 is Element of F2() : F3(b1) in F1() } is set
the Element of { b1 where b1 is Element of F2() : F3(b1) in F1() } is Element of { b1 where b1 is Element of F2() : F3(b1) in F1() }
l1 is Element of F2()
F3(l1) is set
X is non empty set
{ [F3(b1),b1] where b1 is Element of F2() : verum } is set
l1 is set
l2 is set
i1 is Element of F2()
F3(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 F2()
F3(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 F2()
F3(B) is set
[F3(B),B] is V25() set
{F3(B),B} is non empty set
{F3(B)} is non empty trivial 1 -element set
{{F3(B),B},{F3(B)}} is non empty set
e is Element of F2()
F3(e) is set
[F3(e),e] is V25() set
{F3(e),e} is non empty set
{F3(e)} is non empty trivial 1 -element set
{{F3(e),e},{F3(e)}} is non empty set
F1() is set
F2() is non empty set
{ F3(b1) where b1 is Element of F2() : b1 in F1() } is set
the Element of { F3(b1) where b1 is Element of F2() : b1 in F1() } is Element of { F3(b1) where b1 is Element of F2() : b1 in F1() }
X is Element of F2()
F3(X) is set
I is non empty set
{ F3(b1) where b1 is Element of F2() : b1 in I } is set
{ [b1,F3(b1)] where b1 is Element of F2() : verum } is set
l1 is set
l2 is set
i1 is Element of F2()
F3(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 F2()
F3(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 F2()
F3(B) is set
[B,F3(B)] is V25() set
{B,F3(B)} is non empty set
{B} is non empty trivial 1 -element set
{{B,F3(B)},{B}} is non empty set
e is Element of F2()
F3(e) is set
[e,F3(e)] is V25() set
{e,F3(e)} is non empty set
{e} is non empty trivial 1 -element set
{{e,F3(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()