:: FINSET_1 semantic presentation

{{},1} is non empty set
bool {} is non empty set
is non empty functional set

F is set
{F} is non empty set

is non empty Relation-like set
bool is non empty set
dom () is non empty functional Element of bool
bool is non empty set
proj2 () is non empty trivial set
proj1 () is non empty set
x is set
() . {} is set
b is set
() . b is set
rng () is non empty trivial Element of bool {F}
bool {F} is non empty set
the set is set
{ the set } is non empty set
F is set

F1() is set

proj1 F is set

F . e is set
F2(e) is set
F3(e) is set
F is set
e is set
F \/ e is set

proj2 x is set
proj1 x is set

proj2 b is set
proj1 b is set

proj1 x is set
proj2 x is set
y is set
z is set
x . z is set

x . Z is set

b . (Z -^ y) is set

y is set
z is set
x . z is set
x . z is set

z is set
b . z is set

b . ((y +^ Z) -^ y) is set
x . (y +^ Z) is set

F is set
{F} is non empty set
F is set
e is set
{F,e} is non empty set
{F} is non empty () set
{e} is non empty () set
{F} \/ {e} is non empty set
F is set
e is set
x is set
{F,e,x} is non empty set
{F} is non empty () set
{e,x} is non empty () set
{F} \/ {e,x} is non empty set
F is set
e is set
x is set
b is set
{F,e,x,b} is non empty set
{F} is non empty () set
{e,x,b} is non empty () set
{F} \/ {e,x,b} is non empty set
F is set
e is set
x is set
b is set
c5 is set
{F,e,x,b,c5} is non empty set
{F} is non empty () set
{e,x,b,c5} is non empty () set
{F} \/ {e,x,b,c5} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
{F,e,x,b,c5,a} is non empty set
{F} is non empty () set
{e,x,b,c5,a} is non empty () set
{F} \/ {e,x,b,c5,a} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
x is set
{F,e,x,b,c5,a,x} is non empty set
{F} is non empty () set
{e,x,b,c5,a,x} is non empty () set
{F} \/ {e,x,b,c5,a,x} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
x is set
y is set
{F,e,x,b,c5,a,x,y} is non empty set
{F} is non empty () set
{e,x,b,c5,a,x,y} is non empty () set
{F} \/ {e,x,b,c5,a,x,y} is non empty set
F is () set
bool F is non empty set
e is Element of bool F
x is set

proj2 b is set
proj1 b is set

proj1 c5 is set
a is set
x is set
b . x is set
c5 . x is set
x is set
c5 . x is set
b . x is set
b . x is set
b . x is set
proj2 c5 is set
F is () set
e is () set
F \/ e is set
F is set
e is set
F is set
e is set
F \/ e is set
F is set
e is () set
F /\ e is set
F is () set
e is set
F /\ e is () set
F \ e is () Element of bool F
bool F is non empty set
F is set
e is set
F /\ e is set
F is set
e is set
F \ e is Element of bool F
bool F is non empty set

e is () set
F .: e is set
proj1 F is set
() /\ e is () set

proj2 b is set
proj1 b is set

proj2 (b * F) is set
proj1 (b * F) is set
F .: (() /\ e) is set
F is set

e .: F is set
F is set
bool F is non empty set
bool (bool F) is non empty set
e is Element of bool (bool F)

proj2 x is set
proj1 x is set
bool () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
b is set
c5 is set
the Element of e is Element of e
x " the Element of e is set
x .: (x " the Element of e) is set
c5 is Element of bool (bool ())
bool () is non empty set
x is Element of bool ()
y is set

bool x is non empty set
bool (bool x) is non empty set

bool (succ x) is non empty set
bool (bool (succ x)) is non empty set
y is Element of bool (bool (succ x))
{x} is non empty () set
bool x is non empty Element of bool (bool x)
z is set
y is set
the Element of y is Element of y
x \/ {x} is non empty set
the Element of y \ {x} is Element of bool the Element of y
bool the Element of y is non empty set
(x \/ {x}) \ {x} is Element of bool (x \/ {x})
bool (x \/ {x}) is non empty set
x \ {x} is Element of bool x
y is Element of bool (bool x)
Z is set
X1 is set
X1 \ {x} is Element of bool X1
bool X1 is non empty set
Z \/ {x} is non empty set
A is non empty set
B is set
B \ {x} is Element of bool B
bool B is non empty set
(B \ {x}) \/ {x} is non empty set
A \ {x} is Element of bool A
bool A is non empty set
Z \ {x} is Element of bool Z
bool Z is non empty set
X1 \/ {x} is non empty set
A is set
B is set
B \ {x} is Element of bool B
bool B is non empty set
A \ {x} is Element of bool A
bool A is non empty set
A \/ {x} is non empty set
(B \ {x}) \/ {x} is non empty set
B \/ {x} is non empty set
x is set
B is set
c17 is set

bool x is non empty set
bool (bool x) is non empty set
y is Element of bool (bool x)
x is set
x .: x is set
y is set
x " (x .: x) is set
x " y is set
x .: (x " y) is set
y is set
F1() is set
bool F1() is non empty Element of bool (bool F1())
bool F1() is non empty set
bool (bool F1()) is non empty set
F is set
e is set
e is Element of bool (bool F1())
x is set
F1() \ x is Element of bool F1()
the Element of F1() \ x is Element of F1() \ x
{ the Element of F1() \ x} is non empty () set
x \/ { the Element of F1() \ x} is non empty set
c5 is set
b is set
F is set
union F is set
bool F is non empty Element of bool (bool F)
bool F is non empty set
bool (bool F) is non empty set
e is set
x is set
b is set
{x} is non empty () set
b \/ {x} is non empty set
union (b \/ {x}) is set
union b is set
union {x} is set
() \/ () is set
() \/ x is set
c5 is set
union c5 is set
x is set
union x is set
F is () set
e is () set
[:F,e:] is Relation-like set
x is set
{x} is non empty () set

proj1 b is set
proj2 b is set
c5 is set
a is set
b . a is set
[a,x] is V1() set
{a,x} is non empty () set
{a} is non empty () set
{{a,x},{a}} is non empty () set
a is set
x is set
[a,x] is V1() set
{a,x} is non empty () set
{a} is non empty () set
{{a,x},{a}} is non empty () set
b . a is set
b .: F is () set
bool [:F,e:] is non empty Element of bool (bool [:F,e:])
bool [:F,e:] is non empty set
bool (bool [:F,e:]) is non empty set
x is set
union x is set
b is set
c5 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
{a} is non empty () set

proj1 b is set
proj2 b is set
c5 is set
a is set
b . a is set
{a} is non empty () set

a is set
{a} is non empty () set

b . a is set
b .: e is () set
c5 is set
a is set
{a} is non empty () set

F is () set
e is () set
x is () set
[:F,e,x:] is set
[:F,e:] is Relation-like () set
[:[:F,e:],x:] is Relation-like () set
F is () set
e is () set
x is () set
b is () set
[:F,e,x,b:] is set
[:F,e,x:] is () set
[:[:F,e,x:],b:] is Relation-like () set
F is () set
bool F is non empty Element of bool (bool F)
bool F is non empty set
bool (bool F) is non empty set
e is set
bool {} is non empty Element of bool ()
bool () is non empty set
x is set
b is set
{x} is non empty () set
b \/ {x} is non empty set
bool b is non empty Element of bool (bool b)
bool b is non empty set
bool (bool b) is non empty set
c5 is set
y is set
a is set
y \/ {x} is non empty set
z is set
x is set
z \/ {x} is non empty set
c5 is set
c5 \/ {x} is non empty set
a is set
a \/ {x} is non empty set

proj1 c5 is set
proj2 c5 is set
bool (b \/ {x}) is non empty set
bool (b \/ {x}) is non empty Element of bool (bool (b \/ {x}))
bool (bool (b \/ {x})) is non empty set
(bool (b \/ {x})) \ (bool b) is Element of bool (bool (b \/ {x}))
a is set
x is set
c5 . x is set
y is set
y \/ {x} is non empty set
a \ {x} is Element of bool a
bool a is non empty set
y is set
c5 . (a \ {x}) is set
y is set
y \/ {x} is non empty set
a \/ {x} is non empty set
c5 .: (bool b) is set
((bool (b \/ {x})) \ (bool b)) \/ (bool b) is non empty set
(bool (b \/ {x})) \/ (bool b) is non empty set
F is set
union F is set
bool () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
e is set

proj1 F is set
proj2 F is set
F .: () is set
F is set

proj2 e is set
e " F is set
e .: (e " F) is set
F is () set
e is () set
F \+\ e is set
F \ e is () set
e \ F is () set
(F \ e) \/ (e \ F) is () set
F is non empty set
bool F is non empty set
the Element of F is Element of F
{ the Element of F} is non empty () Element of bool F

proj1 F is set
proj2 F is set
[:(),():] is Relation-like set
proj2 F is set
[:(),():] is Relation-like set
pr1 ((),()) is Relation-like [:(),():] -defined proj1 F -valued Function-like V18([:(),():], proj1 F) Element of bool [:[:(),():],():]
[:[:(),():],():] is Relation-like set
bool [:[:(),():],():] is non empty set
(pr1 ((),())) .: F is Element of bool ()
bool () is non empty set
F is set
e is set
x is set
{e} is non empty () set
x \/ {e} is non empty set
b is set
c5 is set
b is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
c5 is set
c5 is set
a is set
x is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
{e} is non empty () set
x \/ {e} is non empty set
b is set
e is set
F is set
e is set
x is set
{e} is non empty () set
x \/ {e} is non empty set
b is set
c5 is set
b is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
c5 is set
c5 is set
a is set
x is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
{e} is non empty () set
x \/ {e} is non empty set
b is set
e is set
F is set
e is set
x is set
[:e,x:] is Relation-like set

proj1 b is set

proj1 c5 is set
proj2 b is set
a is set
proj2 c5 is set
x is set
[:a,x:] is Relation-like set
y is set
z is set
b . z is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
z `1 is set
y is set
z is set
c5 . z is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
z `2 is set
y is set
z is set
y is set
[z,y] is V1() set
{z,y} is non empty () set
{z} is non empty () set
{{z,y},{z}} is non empty () set
c5 . y is set
y `2 is set
b . y is set
y `1 is set
F is set
e is set
x is set
[:e,x:] is Relation-like set

proj1 b is set
proj2 b is set
c5 is set
[:c5,x:] is Relation-like set
a is set
x is set
b . x is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
x `1 is set
a is set
x is set
y is set
[x,y] is V1() set
{x,y} is non empty () set
{x} is non empty () set
{{x,y},{x}} is non empty () set
b . a is set
a `1 is set
is V1() set
is non empty functional () set
is non empty () set
is non empty Relation-like Function-like () set
F is Relation-like () set
proj1 F is set

proj1 e is set
x is set
proj2 e is set
b is set
e . b is set
b `2 is set
[x,(b `2)] is V1() set
{x,(b `2)} is non empty () set
{x} is non empty () set
{{x,(b `2)},{x}} is non empty () set
b `1 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
b is set
[x,b] is V1() set
{x,b} is non empty () set
{x} is non empty () set
{{x,b},{x}} is non empty () set
e . [x,b] is set
[x,b] `1 is set

proj1 (e * F) is set
proj1 e is () set
F is () set
e is set
[:F,e:] is Relation-like set
bool [:F,e:] is non empty set
x is Relation-like F -defined e -valued Function-like V18(F,e) Element of bool [:F,e:]
dom x is () Element of bool F
bool F is non empty () set
F is set
e is set

{F} is non empty () set
{F} --> e is non empty Relation-like {F} -defined {e} -valued Function-like constant V17({F}) V18({F},{e}) () Element of bool [:{F},{e}:]
{e} is non empty () set
[:{F},{e}:] is non empty Relation-like () set
bool [:{F},{e}:] is non empty () set
F is Relation-like () set
proj2 F is set

proj1 e is set
x is set
proj2 e is set
b is set
e . b is set
b `1 is set
[(b `1),x] is V1() set
{(b `1),x} is non empty () set
{(b `1)} is non empty () set
{{(b `1),x},{(b `1)}} is non empty () set
b `2 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
b is set
[b,x] is V1() set
{b,x} is non empty () set
{b} is non empty () set
{{b,x},{b}} is non empty () set
e . [b,x] is set
[b,x] `2 is set

e is set
F " e is set
proj1 F is () set

proj1 (F +* e) is set
proj1 F is () set
proj1 e is () set
() \/ () is () set

proj1 F is set
e is set
F . e is set
proj2 F is set
F . e is set
e is set
proj2 F is set
x is set
F . x is set
F is set

x is set
dom e is Element of bool F
bool F is non empty set
e . x is set
dom e is Element of bool F
bool F is non empty set
e . x is set
dom e is Element of bool F
bool F is non empty set
x is set
proj1 e is set
e . x is set
dom e is Element of bool F
bool F is non empty set
F is set
e is set
[:e,F:] is Relation-like set
x is set
{x} is non empty () set
[x,{x}] is V1() set
{x,{x}} is non empty () set
{{x,{x}},{x}} is non empty () set
F is set

F is set
e is set
F is non empty set
e is non empty set
the Element of F is Element of F
the Element of e is Element of e
{ the Element of F} is non empty () set
the Element of F .--> the Element of e is Relation-like F -defined { the Element of F} -defined e -valued Function-like one-to-one () set
{ the Element of F} --> the Element of e is non empty Relation-like { the Element of F} -defined e -valued { the Element of e} -valued Function-like constant V17({ the Element of F}) V18({ the Element of F},{ the Element of e}) () Element of bool [:{ the Element of F},{ the Element of e}:]
{ the Element of e} is non empty () set
[:{ the Element of F},{ the Element of e}:] is non empty Relation-like () set
bool [:{ the Element of F},{ the Element of e}:] is non empty () set
c5 is Relation-like F -defined { the Element of F} -defined e -valued Function-like one-to-one () set
F is set
e is Relation-like () set

e is Relation-like () set
F is set

F is () set

proj1 (e | F) is set
F is Relation-like () set
field F is set
proj1 F is () set
proj2 F is () set
() \/ () is () set
F is set
e is set
{e} is non empty () set
F is set
F is non trivial set
bool F is non empty set
e is set
x is set
{e,x} is non empty () set
b is Element of bool F
F is set
e is set
x is set
b is set
(F,e) --> (x,b) is set

{F} is non empty () set
{F} --> x is non empty Relation-like {F} -defined {x} -valued Function-like constant V17({F}) V18({F},{x}) () Element of bool [:{F},{x}:]
{x} is non empty () set
[:{F},{x}:] is non empty Relation-like () set
bool [:{F},{x}:] is non empty () set

{e} is non empty () set
{e} --> b is non empty Relation-like {e} -defined {b} -valued Function-like constant V17({e}) V18({e},{b}) () Element of bool [:{e},{b}:]
{b} is non empty () set
[:{e},{b}:] is non empty Relation-like () set
bool [:{e},{b}:] is non empty () set
(F .--> x) +* (e .--> b) is Relation-like Function-like () set
F is set
e is set
F is () set
e is Element of F
is non empty () set
F is non empty () set
e is set
F is () set
{F} is non empty () set
e is set
bool F is non empty () Element of bool (bool F)
bool F is non empty () set
bool (bool F) is non empty () set
e is set
e is () set
{F,e} is non empty () set
x is set
F is () set
bool F is non empty set
e is Element of bool F
x is set
e is () set
F \/ e is set
x is set
F is () () set
union F is set
e is set
is non empty () () set

is non empty Relation-like () set
bool is non empty () () set

e is set
F . e is set

e is set
proj2 F is set

e is set
F . e is set
proj1 F is set
proj1 F is set
proj1 F is set
F is Relation-like () set
proj2 F is set
e is set