:: 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

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

F

F

[:F

[:[:F

bool [:[:F

I is Element of [:F

I `1 is Element of F

I `2 is Element of F

F

I is non empty Relation-like [: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 V25() Element of [:F

[X,l1] `1 is Element of F

[X,l1] `2 is Element of F

F

F

{ F

the Element of { F

X is Element of F

F

F

I is non empty set

{ b

{ b

{ F

l2 is set

i1 is Element of F

F

F

l2 is set

i1 is Element of F

F

i2 is Element of F

F

{ [F

l2 is set

i1 is set

i2 is Element of I

B is Element of F

F

B is Element of F

F

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

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

[F

{F

{F

{{F

l is Element of F

F

[F

{F

{F

{{F

bool I is non empty set

F

F

{ b

the Element of { b

l1 is Element of F

F

X is non empty set

{ [F

l1 is set

l2 is set

i1 is Element of F

F

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

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

[F

{F

{F

{{F

e is Element of F

F

[F

{F

{F

{{F

F

F

{ F

the Element of { F

X is Element of F

F

I is non empty set

{ F

{ [b

l1 is set

l2 is set

i1 is Element of F

F

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

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,F

{B,F

{B} is non empty trivial 1 -element set

{{B,F

e is Element of F

F

[e,F

{e,F

{e} is non empty trivial 1 -element set

{{e,F

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()