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

RAT is set
INT is 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

Seg 3 is non empty finite 3 -element Element of bool NAT
{1,2,3} is non empty set

proj2 I is set
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

proj1 I is set
[:(),X:] is Relation-like set
bool [:(),X:] is non empty set

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

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

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

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

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

proj1 I is set
X is set
{X} is non empty trivial 1 -element set

I . X is 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} is non empty trivial 1 -element set

{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} is non empty trivial 1 -element set

{l1} is non empty trivial 1 -element set
[:{I},{l1}:] is non empty Relation-like set
bool [:{I},{l1}:] is non empty set

{X} is non empty trivial 1 -element set

{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

l1 is set
X . l1 is 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

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

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]} --> (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

proj2 l1 is set

proj1 I is set

(X +* 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 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 (#) (X +* 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 l1) is set
proj1 I is set
l2 is set
I . l2 is set
proj1 X is set
proj1 l1 is set
() \/ (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

proj2 I is set

proj1 X is set

I (#) (l1 +* 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

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
l1 is set

{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} is non empty trivial 1 -element set

{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

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

proj1 l1 is set

l1 . X is 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 | I) +* (l1 | {X}) is Relation-like Function-like set

X is set
l1 is set

{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

{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
() \/ X is set
proj1 ((I +* (X --> l1)) +* (X --> l2)) is set
(() \/ X) \/ X is set
X \/ X is set
() \/ (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

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

I is set

l1 is set
I is set
I is set

X is set

proj2 <*I*> is non empty trivial 1 -element set
{I} is non empty trivial 1 -element set
I is set

X is set

l1 is 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

len I is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT

len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
dom X is V92() Element of bool NAT
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

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

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

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

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

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 non empty trivial functional 1 -element set
[:(Seg I),{X}:] is Relation-like set
bool [:(Seg I),{X}:] is non empty 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 ^ 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

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

X is set

<*X*> . 1 is 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

X is set
proj1 I is set
() \ X is Element of bool ()
bool () is non empty set
I | (() \ X) is Relation-like Function-like set

l1 is set
proj1 I is set
() \ l1 is Element of bool ()
bool () is non empty set
I | (() \ l1) is Relation-like Function-like set
proj1 X is set
() \ l1 is Element of bool ()
bool () is non empty set
X | (() \ l1) is Relation-like Function-like set

l2 is set
proj1 I is set
() \ l2 is Element of bool ()
bool () is non empty set
I | (() \ l2) is Relation-like Function-like set
proj1 X is set
() \ l2 is Element of bool ()
bool () is non empty set
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

proj1 I is set
proj1 X is set
l1 is set
() \ l1 is Element of bool ()
bool () is non empty set
() \ l1 is Element of bool ()
bool () is non empty set
I | (() \ l1) is Relation-like Function-like set
X | (() \ l1) is Relation-like Function-like set
() /\ (() \ l1) is Element of bool ()
proj1 (I | (() \ l1)) is set
() /\ (() \ l1) is Element of bool ()

proj1 X is 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
() \/ () is set
(() \/ ()) \ l1 is Element of bool (() \/ ())
bool (() \/ ()) is non empty set
() \ l1 is Element of bool ()
bool () is non empty set
() \ l1 is Element of bool ()
bool () is non empty set
(() \ l1) \/ (() \ l1) is set
(() \ l1) \/ {} is set
I | (() \ l1) is Relation-like Function-like set
(I +* X) | ((proj1 (I +* X)) \ l1) is Relation-like Function-like set
X is set

proj1 I is set
l1 is set

{X} is non empty trivial 1 -element set

{l1} is non empty trivial 1 -element set
[:{X},{l1}:] is non empty Relation-like set
bool [:{X},{l1}:] is non empty set
I +* (X .--> l1) is non empty Relation-like Function-like set

proj1 I 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

{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
() \/ (dom (l1 .--> X)) is non empty set
() \/ {l1} is non empty 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

{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

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

{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

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

{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

{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

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

{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

{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

X is set
I . X is set
(I,X,(I . X)) is Relation-like Function-like set
proj1 I is set

{X} is non empty trivial 1 -element set
{X} --> (I . X) is non empty Relation-like {X} -defined {(I . X)} -valued Function-like constant total quasi_total Element of bool [:{X},{(I . X)}:]
{(I . X)} is non empty trivial 1 -element set
[:{X},{(I . X)}:] is non empty Relation-like set
bool [:{X},{(I . X)}:] is non empty set

I +* (X .--> (I . X)) is non empty Relation-like Function-like set
proj1 I is set
proj1 I is set

X is set
l1 is set
(I,X,l1) is Relation-like Function-like set
proj1 (I,X,l1) is set
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

I is set

l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l2 is Element of I

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} is non empty trivial 1 -element set

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

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) /. 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

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) /. 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

i1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
X /. i1 is Element of I

dom X is V92() Element of bool NAT
X . i1 is set

dom X is V92() Element of bool NAT
dom X is V92() Element of bool NAT

len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
I is set

[:I,I:] is Relation-like set
bool [:I,I:] is non empty set
dom X is V92() Element of bool NAT

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

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

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

l2 . (len X) is set
i2 is set
l2 . i2 is 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

X . (B + 1) is Relation-like Function-like set
i2 . (B + 1) is Relation-like Function-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

i1 is set

l2 . i1 is 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

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 . (l1 . l2) is set

i2 . (l1 . l2) is set

len l1 is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
l1 . 1 is 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

0 + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT

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,I:] is Relation-like set
bool [:I,I:] is non empty set

I is 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

(I,X) is Relation-like Function-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

[: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 . (len (X ^ <*l1*>)) 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

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

dom <*l1*> is non empty trivial 1 -element V92() Element of bool NAT
I is set

len X is V18() V19() V20() V24() ext-real non negative V37() V38() V39() finite cardinal Element of NAT
(len X) + 1 is non empty V18() V19() V20() V24() ext-real positive non negative V37() V38() V39() finite cardinal Element of NAT
(X,I) . ((len X) + 1) is 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

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

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