:: CLASSES1 semantic presentation

bool omega is non empty set

f is set
g is set
bool g is non empty Element of bool (bool g)
bool g is non empty set
bool (bool g) is non empty set
h is set
meet h is set
I is set
I is set
c6 is set
y is set
I is set
bool I is non empty Element of bool (bool I)
bool I is non empty set
bool (bool I) is non empty set
c6 is set
I is set
c6 is set
I is set
(meet h) /\ I is set
c6 is set
y is set
c6 is set
bool c6 is non empty Element of bool (bool c6)
bool c6 is non empty set
bool (bool c6) is non empty set
c6 is set
c6 is set
g is set
h is set
f is set
(f) is set
f is set

g is set
bool g is non empty Element of bool (bool g)
bool g is non empty set
bool (bool g) is non empty set
g is set

g is set

g is set

f is set
(f) is non empty set
f is set
g is set
(g) is non empty set
h is 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
g is set
(g) is non empty set
f is set
g is set
(g) is non empty set
f is set

g is set
(g) is non empty set
card (g) is cardinal set

{g} is non empty set
g \/ {g} is non empty set
f is set
{f} is non empty set
(f) is non empty set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in a2 & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in a2 } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in a2 & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in a2 } is set

f is set
(f) is non empty set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in a2 & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in a2 } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in a2 & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in a2 } is set

{f} is non empty set
h is set

(f,g) is set

{g} is non empty set
g \/ {g} is non empty set
I is set

last c6 is set

{p} is non empty set
p \/ {p} is non empty set
c6 . {} is set
(f,p) is set
(f,{}) is set

(f,g) is set

rng h is set
union (rng h) is set
(union (rng h)) /\ (f) is set
f is set

(f,g) is set
(f) is non empty set
bool (f) is non empty set
{f} is non empty set
h is set
(f,{}) is set

(f,h) is set

{h} is non empty set
h \/ {h} is non empty set
(f,(succ h)) is set
c6 is set
p is Element of bool (f)
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in p & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in p } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in p & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in p } is set

bool p is non empty set
bool p is non empty Element of bool (bool p)
bool (bool p) is non empty set
(bool p) /\ (f) is Element of bool (bool p)
( { b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in p & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in p }
)
\/ ((bool p) /\ (f)) is set

y is Element of (f)
f is Element of (f)
y is Element of (f)
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty set

(f,h) is set

rng p is set
union (rng p) is set
(union (rng p)) /\ (f) is set
f is set
(f,{}) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set
{f} is non empty set
f is set

{g} is non empty set
g \/ {g} is non empty set
(f,(succ g)) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set
(f,g) is Element of bool (f)
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set

bool (f,g) is non empty set
bool (f,g) is non empty Element of bool (bool (f,g))
bool (bool (f,g)) is non empty set
(bool (f,g)) /\ (f) is Element of bool (bool (f,g))
( { b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) }
)
\/ ((bool (f,g)) /\ (f)) is set

f is set
(f) is non empty set

(f,g) is Element of bool (f)
bool (f) is non empty set
{ b1 where b1 is Element of (f) : ex b2 being epsilon-transitive epsilon-connected ordinal set st
( b2 in g & b1 in (f,b2) )
}
is set

rng h is set
union (rng h) is set
(union (rng h)) /\ (f) is set
p is set
I is set
c6 is set
h . c6 is set

(f,y) is Element of bool (f)
p is set
I is Element of (f)

(f,c6) is Element of bool (f)

(f,c6) is Element of bool (f)
h . c6 is set
f is set
g is set
(g) is non empty set

{h} is non empty set
h \/ {h} is non empty set
(g,(succ h)) is Element of bool (g)
bool (g) is non empty set
(g,h) is Element of bool (g)
{ b1 where b1 is Element of (g) : ex b2 being Element of (g) st
( b2 in (g,h) & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (g) : b1 in (g,h) } is set
bool (g,h) is non empty set
bool (g,h) is non empty Element of bool (bool (g,h))
bool (bool (g,h)) is non empty set
(bool (g,h)) /\ (g) is Element of bool (bool (g,h))
{ b1 where b1 is Element of (g) : ex b2 being Element of (g) st
( b2 in (g,h) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (g) : b1 in (g,h) } is set

( { b1 where b1 is Element of (g) : ex b2 being Element of (g) st
( b2 in (g,h) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (g) : b1 in (g,h) }
)
\/ ((bool (g,h)) /\ (g)) is set

y is Element of (g)
f is Element of (g)
y is Element of (g)
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty set
y is set
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty 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
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
y is set
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty set
f is Element of (g)
f1 is Element of (g)
bool f is non empty Element of bool (bool f)
bool f is non empty set
bool (bool f) is non empty set
y is set
bool y is non empty Element of bool (bool y)
bool y is non empty set
bool (bool y) is non empty set
f is set
g is set
h is set

(h,p) is Element of bool (h)
(h) is non empty set
bool (h) is non empty set

{p} is non empty set
p \/ {p} is non empty set
(h,(succ p)) is Element of bool (h)
f is set
g is set

(g,h) is Element of bool (g)
(g) is non empty set
bool (g) is non empty set
bool f is non empty Element of bool (bool f)
bool f is non empty set
bool (bool f) is non empty set

{h} is non empty set
h \/ {h} is non empty set
(g,(succ h)) is Element of bool (g)
f is set
g is set

(f,h) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set
{ b1 where b1 is Element of (f) : ex b2 being epsilon-transitive epsilon-connected ordinal set st
( b2 in h & b1 in (f,b2) )
}
is set

p is Element of (f)

(f,I) is Element of bool (f)

(f,p) is Element of bool (f)
I is Element of (f)
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
g is set
h is set

(g,p) is Element of bool (g)
(g) is non empty set
bool (g) is non empty set

(g,I) is Element of bool (g)

{I} is non empty set
I \/ {I} is non empty set
(g,(succ I)) is Element of bool (g)
f is set

(f,g) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set

{g} is non empty set
g \/ {g} is non empty set
(f,(succ g)) is Element of bool (f)
h is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set

bool (f,g) is non empty set
bool (f,g) is non empty Element of bool (bool (f,g))
bool (bool (f,g)) is non empty set
(bool (f,g)) /\ (f) is Element of bool (bool (f,g))
( { b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) }
)
\/ ((bool (f,g)) /\ (f)) is set

f is set

(f,g) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set

(f,h) is Element of bool (f)

(f,p) is Element of bool (f)
I is set

{c6} is non empty set
c6 \/ {c6} is non empty set
(f,c6) is Element of bool (f)
{ b1 where b1 is Element of (f) : ex b2 being epsilon-transitive epsilon-connected ordinal set st
( b2 in p & b1 in (f,b2) )
}
is set

{c6} is non empty set
c6 \/ {c6} is non empty set
f is set
(f) is non empty set
g is set
h is set
p is set
I is set

{c6} is non empty set
c6 \/ {c6} is non empty set
(f,(succ c6)) is Element of bool (f)
bool (f) is non empty set
(f,c6) is Element of bool (f)

{y} is non empty set
y \/ {y} is non empty set
(f,(succ y)) is Element of bool (f)
(f,y) is Element of bool (f)
h is set

(f,p) is Element of bool (f)
bool (f) is non empty set

{p} is non empty set
p \/ {p} is non empty set
(f,(succ p)) is Element of bool (f)
I is set
f is set
(f) is non empty set

(f,g) is Element of bool (f)
bool (f) is non empty set

{g} is non empty set
g \/ {g} is non empty set
(f,(succ g)) is Element of bool (f)
(f,{}) is Element of bool (f)
{f} is non empty set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set
{ b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) } is set

bool (f,g) is non empty set
bool (f,g) is non empty Element of bool (bool (f,g))
bool (bool (f,g)) is non empty set
(bool (f,g)) /\ (f) is Element of bool (bool (f,g))
( { b1 where b1 is Element of (f) : ex b2 being Element of (f) st
( b2 in (f,g) & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of (f) : b1 in (f,g) }
)
\/ ((bool (f,g)) /\ (f)) is set

h is set
p is set
I is Element of (f)
c6 is Element of (f)
h is set
bool h is non empty Element of bool (bool h)
bool h is non empty set
bool (bool h) is non empty set
h is set
f is set
(f) is non empty set

(f,g) is Element of bool (f)
bool (f) is non empty set

{g} is non empty set
g \/ {g} is non empty set
(f,(succ g)) is Element of bool (f)
f is set
(f) is non empty set

(f,g) is Element of bool (f)
bool (f) is non empty set

(f,h) is Element of bool (f)
f is set
g is set
(g) is non empty set

(g,h) is Element of bool (g)
bool (g) is non empty set

(g,h) is Element of bool (g)
bool (g) is non empty set
{g} is non empty set
(g,{}) is Element of bool (g)

(g,p) is Element of bool (g)

{p} is non empty set
p \/ {p} is non empty set
(g,p) is Element of bool (g)
(g,(succ p)) is Element of bool (g)
f is set

(f,g) is Element of bool (f)
(f) is non empty set
bool (f) is non empty set
h is set

{p} is non empty set
p \/ {p} is non empty set
(f,p) is Element of bool (f)
I is set
bool I is non empty Element of bool (bool I)
bool I is non empty set
bool (bool I) is non empty set
c6 is set
c6 is set
{f} is non empty set

(f,p) is Element of bool (f)

{p} is non empty set
p \/ {p} is non empty set
(f,(succ p)) is Element of bool (f)

{p} is non empty set
p \/ {p} is non empty set
f is set
(f) is non empty set

(f,g) is Element of bool (f)
bool (f) is non empty set

{g} is non empty set
g \/ {g} is non empty set
(f,(succ g)) is Element of bool (f)
f is set

g is set
(g) is non empty set
card (g) is cardinal set
bool f is non empty Element of bool (bool f)
bool f is non empty set
bool (bool f) is non empty set
h is set
card (bool f) is cardinal set
f is set
g is set
(g) is non empty set

card (g) is cardinal set
f is set
(f) is non empty set
g is set
{g} is non empty set
h is set
{g,h} is non empty set
bool g is non empty Element of bool (bool g)
bool g is non empty set
bool (bool g) is non empty set
bool {g} is non empty Element of bool ()
bool {g} is non empty set
bool () is non empty set
{{},{g}} is non empty set

dom p is set
rng p is set
I is set
c6 is set
p . I is set
p . c6 is set
I is set
c6 is set
p . c6 is set
I is set
p . {} is set
p . {g} is set
f is set
(f) is non empty set
g is set
h is set
[g,h] is set
{g,h} is non empty set
{g} is non empty set
{{g,h},{g}} is non empty set
f is set
g is set
(g) is non empty set
h is set
[:f,h:] is Relation-like set
p is set
I is set
[p,I] is set
{p,I} is non empty set
{p} is non empty set
{{p,I},{p}} is non empty set

{f} is non empty set
f \/ {f} is non empty set
g is set

(f) is set

{f} is non empty set
f \/ {f} is non empty set
p is set

last I is set

{h} is non empty set
h \/ {h} is non empty set
I . {} is set
(h) is set
({}) is set

(f) is set

rng g is set
union (rng g) is set

{f} is non empty set
f \/ {f} is non empty set
((succ f)) is 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

(f) is set

rng g is set
union (rng g) is set
h is set
p is set
I is set
g . I is set

(c6) is set

(p) is set
g . p is set
f is set

(g) is set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is set
bool (g) is non empty Element of bool (bool (g))
bool (g) is non empty set
bool (bool (g)) is non empty set
bool (g) is non empty Element of bool (bool (g))
bool (g) is non empty set
bool (bool (g)) is non empty set

(f) is set

(g) is set
h is set
p is set

(I) is set

{I} is non empty set
I \/ {I} is non empty set
(I) is set
g is set

(f) is epsilon-transitive set

{f} is non empty set
f \/ {f} is non empty set
((succ f)) is epsilon-transitive set
bool (f) is non empty Element of bool (bool (f))
bool (f) is non empty set
bool (bool (f)) is non empty set

(f) is epsilon-transitive set
union (f) is set
g is set
h is set
f is set
union f is set

(g) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set
(h) is epsilon-transitive set
union (h) is set

(h) is epsilon-transitive set
union (h) is set

{h} is non empty set
h \/ {h} is non empty set
((succ h)) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set

(f) is epsilon-transitive set

(g) is epsilon-transitive set

(h) is epsilon-transitive set

(p) is epsilon-transitive set

{I} is non empty set
I \/ {I} is non empty set
(I) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set
((succ h)) is epsilon-transitive set

{I} is non empty set
I \/ {I} is non empty set

(f) is epsilon-transitive set

(g) is epsilon-transitive set

(f) is epsilon-transitive set

(g) is epsilon-transitive set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set

(g) is epsilon-transitive set
h is set

{p} is non empty set
p \/ {p} is non empty set
(p) is epsilon-transitive set
((succ p)) is epsilon-transitive set

(f) is epsilon-transitive set
g is set

{h} is non empty set
h \/ {h} is non empty set
((succ h)) is epsilon-transitive set
(h) is epsilon-transitive set
bool (h) is non empty Element of bool (bool (h))
bool (h) is non empty set
bool (bool (h)) is non empty set

(h) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set

(f) is epsilon-transitive set
card (f) is cardinal set
g is 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

(g) is epsilon-transitive set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set
h is set
bool (g) is non empty Element of bool (bool (g))
bool (g) is non empty set
bool (bool (g)) is non empty set
h is set
{h} is non empty set
bool (g) is non empty Element of bool (bool (g))
bool (g) is non empty set
bool (bool (g)) is non empty set
f is set
g is set

(h) is epsilon-transitive set

{p} is non empty set
p \/ {p} is non empty set
((succ p)) is epsilon-transitive set
(p) is epsilon-transitive set
bool (p) is non empty Element of bool (bool (p))
bool (p) is non empty set
bool (bool (p)) is non empty set

(p) is epsilon-transitive set
bool (p) is non empty Element of bool (bool (p))
bool (p) is non empty set
bool (bool (p)) is non empty set

{p} is non empty set
p \/ {p} is non empty set
((succ p)) is epsilon-transitive set

{p} is non empty set
p \/ {p} is non empty 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

(g) is epsilon-transitive set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set
h is set
f is set
{f} is non empty set

(g) is epsilon-transitive set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set
f is set
g is set
{f,g} is non empty set

(h) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set
((succ h)) is epsilon-transitive set
f is set
g is set
[f,g] is set
{f,g} is non empty set
{f} is non empty set
{{f,g},{f}} is non empty set

(h) is epsilon-transitive set

{h} is non empty set
h \/ {h} is non empty set

{(succ h)} is non empty set
(succ h) \/ {(succ h)} is non empty set
((succ (succ h))) is epsilon-transitive set
((succ h)) is epsilon-transitive set
f is set
(f) is non empty set

(g) is epsilon-transitive set
(g) /\ (f) is set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set
((succ g)) /\ (f) is set
h is set
(f) \ (g) is Element of bool (f)
bool (f) is non empty set
p is set
I is set
f is set
(f) is non empty set
g is set
h is set
p is set
I is set

(c6) is epsilon-transitive set

{c6} is non empty set
c6 \/ {c6} is non empty set
((succ c6)) is epsilon-transitive set

(y) is epsilon-transitive set

{y} is non empty set
y \/ {y} is non empty set
((succ y)) is epsilon-transitive set
h is set

(p) is epsilon-transitive set
(p) /\ (f) is set

{p} is non empty set
p \/ {p} is non empty set
((succ p)) is epsilon-transitive set
((succ p)) /\ (f) is set
I is set
f is set
union f is set
g is set
h is set
f is set
g is set
f \/ g is set
h is set
f is set
g is set
f /\ g is set
h is set
f is set

dom g is set
g . {} is set
rng g is set
union (rng g) is set
h is set
p is set
I is set
c6 is set
g . c6 is set

g . y is set

{f} is non empty set
f \/ {f} is non empty set
g . (succ f) is set
g . f is set
union (g . f) is set

I . c6 is set
dom I is set
I . {} is set

{y} is non empty set
y \/ {y} is non empty set
g . (succ y) is set
g . y is set
union (g . y) is set
g is set
h is set
f is set
(f) is set
g is set

h . p is set
dom h is set
h . {} is set

{p} is non empty set
p \/ {p} is non empty set
h . (succ p) is set
union (h . p) is set
I is set

h . c6 is set
f is set
(f) is set
g is set

dom h is set
h . {} is set

h . p is set
f is set
(f) is set
g is set
h is set

p . I is set
dom p is set
p . {} is set

p . c6 is set

{c6} is non empty set
c6 \/ {c6} is non empty set
p . (succ c6) is set
union (p . c6) is set
union g is set
f is set
(f) is set
g is set
f is set
(f) is set
g is set
({}) is set

(f) is set
f is set
(f) is set
g is set
(g) is set
f is set
(f) is set
((f)) is set
f is set
(f) is set
g is set
f \/ g is set
((f \/ g)) is set
(g) is set
(f) \/ (g) is set
(((f) \/ (g))) is set
f is set
(f) is set
g is set
f /\ g is set
((f /\ g)) is set
(g) is set
(f) /\ (g) is set
f is set
(f) is set
((f)) is non empty set

(g) is epsilon-transitive set
f is set

(g) is epsilon-transitive set

(h) is epsilon-transitive 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

{(f)} is non empty set
(f) \/ {(f)} is non empty set
((f)) is epsilon-transitive set
((succ (f))) is epsilon-transitive set
g 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

(g) is epsilon-transitive set

(h) is epsilon-transitive set

(p) is epsilon-transitive set

{p} is non empty set
p \/ {p} is non empty set

{p} is non empty set
p \/ {p} is non empty set
(p) is epsilon-transitive set

(f) is epsilon-transitive set

(g) is epsilon-transitive set
f is set

(g) is epsilon-transitive set
((f)) is epsilon-transitive set
f is set

(g) is epsilon-transitive set
bool f is non empty Element of bool (bool f)
bool f is non empty set
bool (bool f) is non empty set

{g} is non empty set
g \/ {g} is non empty set
((succ g)) is epsilon-transitive set

{(f)} is non empty set
(f) \/ {(f)} is non empty set

{(f)} is non empty set
(f) \/ {(f)} is non empty set
((f)) is epsilon-transitive set
((succ (f))) is epsilon-transitive set
f is set

g is set

((g)) is epsilon-transitive set
f is set

g is set

((g)) is epsilon-transitive set
f is set

((f)) is epsilon-transitive set
p is set

(g) is epsilon-transitive set
(g) is epsilon-transitive set
p is set

f is set

(h) is epsilon-transitive set
f \ (h) is Element of bool f
bool f is non empty set
the Element of f \ (h) is Element of f \ (h)
( the Element of f \ (h)) is epsilon-transitive epsilon-connected ordinal set
h is set

I is set

f is set

g is set

f is set

{g} is non empty set
g \/ {g} is non empty set
h is set

(f) is epsilon-transitive set

p is set
I is set

f is set
(f) is non empty set

(((f))) is epsilon-transitive set

{g} is non empty set
g \/ {g} is non empty set
h is set

bool h is non empty Element of bool (bool h)
bool h is non empty set
bool (bool h) is non empty set

(g) is epsilon-transitive set
F1() is set
f is set

dom f is set
rng f is set
f is non empty set
g is Element of f
h is set

((h)) is epsilon-transitive set

{(h)} is non empty set
(h) \/ {(h)} is non empty set
((succ (h))) is epsilon-transitive set

dom g is set
rng g is set

((sup (rng g))) is epsilon-transitive set
h is set
g . h is set

(p) is epsilon-transitive set
I is set
I is set

dom h is set
rng h is set

p is set
Coim (h,p) is set
{p} is non empty set
h " {p} is set
card (Coim (h,p)) is cardinal set

I is set
Coim (p,I) is set
{I} is non empty set
p " {I} is set
card (Coim (p,I)) is cardinal set
Coim (h,I) is set
h " {I} is set
card (Coim (h,I)) is cardinal set

rng f is set
g is set
Coim (f,g) is set
{g} is non empty set
f " {g} is set
h is set

rng f is set
rng g is set
h is set
Coim (f,h) is set
{h} is non empty set
f " {h} is set
card (Coim (f,h)) is cardinal set
Coim (g,h) is set
g " {h} is set
card (Coim (g,h)) is cardinal set
dom f is set
p is set
f . p is set
h is set
Coim (g,h) is set
{h} is non empty set
g " {h} is set
card (Coim (g,h)) is cardinal set
Coim (f,h) is set
f " {h} is set
card (Coim (f,h)) is cardinal set
dom g is set
p is set
g . p is set

p is set
Coim (g,p) is set
{p} is non empty set
g " {p} is set
card (Coim (g,p)) is cardinal set
Coim (h,p) is set
h " {p} is set
card (Coim (h,p)) is cardinal set
Coim (f,p) is set
f " {p} is set
card (Coim (f,p)) is cardinal set

dom f is set
dom g is set
rng f is set
h is set
{h} is non empty set
f " {h} is set
g " {h} is set
Coim (f,h) is set
card (Coim (f,h)) is cardinal set
Coim (g,h) is set
card (Coim (g,h)) is cardinal set

dom p is set
rng p is set

dom I is set
rng I is set

dom h is set
c6 is set
f . c6 is set
h . (f . c6) is set

dom y is set
{(f . c6)} is non empty set
f " {(f . c6)} is set
rng y is set
g " {(f . c6)} is set
y . c6 is set
f is set

f1 . c6 is set

dom c6 is set
rng c6 is set

y is set
g . y is set
rng g is set
h . (g . y) is set

dom f is set
{(g . y)} is non empty set
f " {(g . y)} is set
rng f is set
g " {(g . y)} is set
f1 is set
f . f1 is set
f . f1 is set
c6 . f1 is set
y is set
f is set
c6 . y is set
c6 . f is set
f . y is set
f . f is set
h . (f . y) is set
h . (f . f) is set

f1 . y is set

f2 . f is set
dom f1 is set
{(f . y)} is non empty set
f " {(f . y)} is set
rng f1 is set
g " {(f . y)} is set
dom f2 is set
{(f . f)} is non empty set
f " {(f . f)} is set
rng f2 is set
g " {(f . f)} is set
(g " {(f . y)}) /\ (g " {(f . f)}) is set
{(f . y)} /\ {(f . f)} is set
g " ({(f . y)} /\ {(f . f)}) is set
g . (f1 . y) is set
dom (c6 * g) is set
y is set
f . y is set
h . (f . y) is set

dom f is set
{(f . y)} is non empty set
f " {(f . y)} is set
rng f is set
g " {(f . y)} is set
f . y is set
g . (f . y) is set
c6 . y is set
(c6 * g) . y is set

dom h is set
rng h is set

p is set
Coim (f,p) is set
{p} is non empty set
f " {p} is set
card (Coim (f,p)) is cardinal set
Coim (g,p) is set
g " {p} is set
card (Coim (g,p)) is cardinal set
h | (f " {p}) is Relation-like Function-like set
dom (h | (f " {p})) is set
rng (h | (f " {p})) is set
c6 is set
y is set
(h | (f " {p})) . y is set
f . y is set
h . y is set
(dom h) /\ (f " {p}) is set
g . c6 is set
c6 is set
g . c6 is set
y is set
h . y is set
f . y is set
(h | (f " {p})) . y is set

dom f is set
dom g is set

dom h is set
rng h is set

p is set
f " p is set
card (f " p) is cardinal set
g " p is set
card (g " p) is cardinal set
h | (f " p) is Relation-like Function-like set
dom (h | (f " p)) is set
rng (h | (f " p)) is set
c6 is set
y is set
(h | (f " p)) . y is set
f . y is set
h . y is set
(dom h) /\ (f " p) is set
g . c6 is set
c6 is set
g . c6 is set
y is set
h . y is set
f . y is set
(h | (f " p)) . y is set
h is set
Coim (f,h) is set
{h} is non empty set
f " {h} is set
card (Coim (f,h)) is cardinal set
Coim (g,h) is set
g " {h} is set
card (Coim (g,h)) is cardinal set
f is non empty set

rng g is set

rng h is set
p is set
Coim (g,p) is set
{p} is non empty set
g " {p} is set
card (Coim (g,p)) is cardinal set
Coim (h,p) is set
h " {p} is set
card (Coim (h,p)) is cardinal set
I is Element of f
Coim (h,I) is set
{I} is non empty set
h " {I} is set
card (Coim (h,I)) is cardinal set
Coim (g,I) is set
g " {I} is set
card (Coim (g,I)) is cardinal set
dom h is set
c6 is set
h . c6 is set
I is Element of f
Coim (g,I) is set
{I} is non empty set
g " {I} is set
card (Coim (g,I)) is cardinal set
Coim (h,I) is set
h " {I} is set
card (Coim (h,I)) is cardinal set

dom f is set

dom g is set
[:(dom f),(dom f):] is Relation-like set
bool [:(dom f),(dom f):] is non empty set

dom h is set
rng h is set

rng h is set
dom h is set

dom f is set
card (dom f) is cardinal set
dom g is set
card (dom g) is cardinal set
rng f is set
f " (rng f) is set
card (f " (rng f)) is cardinal set
g " (rng f) is set
card (g " (rng f)) is cardinal set
rng g is set
g " (rng g) is set
card (g " (rng g)) is cardinal set
f is set

rng g is set
[g,f] is set
{g,f} is non empty set
{g} is non empty set
{{g,f},{g}} is non empty set

h is set

p is set
[p,h] is set
{p,h} is non empty set
{p} is non empty set
{{p,h},{p}} is non empty set

dom f is set

dom g is set
rng f is set

dom h is set
rng g is set

[:(dom f),(dom f):] is Relation-like set
bool [:(dom f),(dom f):] is non empty set

dom (f * h) is set
dom (g * h) is set