:: FOMODEL4 semantic presentation

REAL is non empty non trivial non finite non empty-membered set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal non empty-membered countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
BOOLEAN is non empty set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal non empty-membered countable denumerable set
bool NAT is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered set
INT is non empty non trivial non finite non empty-membered set

1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT

is non empty non trivial Relation-like non finite non empty-membered set
is non empty V26() set

bool is non empty non trivial non finite non empty-membered set

NAT \/ () is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like non finite non empty-membered set
bool is non empty non trivial non finite non empty-membered set
K281() is V47() V75() L8()
the U1 of K281() is set
K286() is V47() L8()
K287() is V47() V75() M13(K286())
K288() is V47() V75() V97() V154() M16(K286(),K287())
K290() is V47() V75() V97() V99() V101() L8()
K291() is V47() V75() V97() V154() M13(K290())
2 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
{{},1} is non empty finite V36() countable set
is non empty non trivial Relation-like non finite non empty-membered set
bool is non empty non trivial non finite non empty-membered set

bool is non empty set
3 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT

Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

- 2 is non empty complex ext-real non positive negative finite V40() V41() countable set

X is set
C is set
phi is set
Funcs (C,phi) is functional set
bool (Funcs (C,phi)) is non empty set
[:C,phi:] is Relation-like set
bool [:C,phi:] is non empty set
bool (bool [:C,phi:]) is non empty set
bool [:C,phi:] is non empty Element of bool (bool [:C,phi:])
X is V51() V53() eligible Language-like
TermSymbolsOf X is non empty set
the U1 of X is set
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element countable set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite non empty-membered set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite non empty-membered set
the adicity of X " NAT is Element of bool ( the U1 of X \ { the U3 of X})
bool ( the U1 of X \ { the U3 of X}) is non empty set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U2 of X is Element of the U1 of X

[1,()] is non empty V26() set

AtomicFormulaSymbolsOf X is non empty Element of bool ()
bool () is non empty non trivial non finite non empty-membered set

{()} is non empty trivial finite 1 -element countable set
() \ {()} is non empty non trivial non finite non empty-membered Element of bool ()
bool () is non empty non trivial non finite non empty-membered set
() typed\ {()} is Element of bool ()

bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
bool ((() *) \ ) is non empty non trivial non finite non empty-membered Element of bool (bool ((() *) \ ))
bool (bool ((() *) \ )) is non empty non trivial non finite non empty-membered set

proj2 () is set
union () is set
X -multiCat is non empty Relation-like (() *) * -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:((() *) *),(() *):]
(() *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of () *
[:((() *) *),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:((() *) *),(() *):] is non empty non trivial non finite non empty-membered set
() -multiCat is non empty Relation-like (() *) * -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:((() *) *),(() *):]

bool is non empty finite V36() countable set
K295(()) is non empty Relation-like [:(() *),(() *):] -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:[:(() *),(() *):],(() *):]
[:(() *),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
[:[:(() *),(() *):],(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:[:(() *),(() *):],(() *):] is non empty non trivial non finite non empty-membered set
MultPlace K295(()) is non empty Relation-like ((() *) *) \ -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:(((() *) *) \ ),(() *):]
((() *) *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((() *) *)
bool ((() *) *) is non empty non trivial non finite non empty-membered set
((() *) *) typed\ is functional V36() FinSequence-membered Element of bool ((() *) *)
[:(((() *) *) \ ),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(((() *) *) \ ),(() *):] is non empty non trivial non finite non empty-membered set
() +* () is non empty Relation-like Function-like Function-yielding V156() set
((() *) \ ) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (() *) \
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered Element of bool (((() *) \ ) *)
bool (((() *) \ ) *) is non empty non trivial non finite non empty-membered set

[1,Y] is non empty V26() set

[1,phii] is non empty V26() set

1 + 1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable set
1 + 1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
bool (() *) is non empty non trivial non finite non empty-membered set

(() *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of () *
H * is non empty functional V36() FinSequence-membered Element of bool ((() *) *)
bool ((() *) *) is non empty non trivial non finite non empty-membered set

abs (- 2) is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
- (- 2) is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable set

the adicity of X . HH is set
abs (ar HH) is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT

a is non empty set
D2 is Element of a

[1,D2] is non empty V26() set

() -multiCat is non empty Relation-like (() *) * -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:((() *) *),(() *):]
[:((() *) *),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:((() *) *),(() *):] is non empty non trivial non finite non empty-membered set
K295(()) is non empty Relation-like [:(() *),(() *):] -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:[:(() *),(() *):],(() *):]
[:(() *),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
[:[:(() *),(() *):],(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:[:(() *),(() *):],(() *):] is non empty non trivial non finite non empty-membered set
MultPlace K295(()) is non empty Relation-like ((() *) *) \ -defined () * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:(((() *) *) \ ),(() *):]
((() *) *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((() *) *)
((() *) *) typed\ is functional V36() FinSequence-membered Element of bool ((() *) *)
[:(((() *) *) \ ),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(((() *) *) \ ),(() *):] is non empty non trivial non finite non empty-membered set
() +* () is non empty Relation-like Function-like Function-yielding V156() set

X is V51() V53() eligible Language-like

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
X is V51() V53() eligible Language-like
(X) is set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set

[] is non empty V26() Element of [:(),((() *) \ ):]
[:(),((() *) \ ):] is non empty non trivial Relation-like non finite non empty-membered set
X is V51() V53() eligible Language-like
(X) is non empty set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
DD is set

[FF,D] is non empty V26() Element of [:(),((() *) \ ):]
[:(),((() *) \ ):] is non empty non trivial Relation-like non finite non empty-membered set
bool () is non empty Element of bool ()
bool () is non empty set
[:(),((() *) \ ):] is non empty non trivial Relation-like bool () -defined () * -valued non finite non empty-membered Element of bool [:(),(() *):]
[:(),(() *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(),(() *):] is non empty non trivial non finite non empty-membered set
bool [:(),((() *) \ ):] is non empty non trivial non finite non empty-membered set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty set
C is Relation-like Element of bool (X)
C is Element of (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
the (X) Element of (X) is (X) Element of (X)
bool (X) is non empty set
the Relation-like (X) Element of bool (X) is Relation-like (X) Element of bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
the (X) Element of (X) is (X) Element of (X)
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty set
the Relation-like (X) Element of bool (X) is Relation-like (X) Element of bool (X)
X is set
C is set
Funcs (X,C) is functional set
bool (Funcs (X,C)) is non empty set
phi is functional Element of bool (Funcs (X,C))

X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))

X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))

[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
DD is Relation-like bool (X) -defined bool (X) -valued Element of bool [:(bool (X)),(bool (X)):]
FF is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
D is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
Y is Relation-like (X) Element of bool (X)
D . Y is Relation-like (X) Element of bool (X)
{Y} is non empty trivial finite 1 -element countable Element of bool (bool (X))
bool (bool (X)) is non empty set
() .: {Y} is set
union (() .: {Y}) is set
DD is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
FF is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
D is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
phii is Relation-like (X) Element of bool (X)
D . phii is Relation-like (X) Element of bool (X)
{phii} is non empty trivial finite 1 -element countable set
() .: {phii} is set
union (() .: {phii}) is set
Y is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
Y . phii is Relation-like (X) Element of bool (X)
X is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set
C is V51() V53() eligible Language-like
(C) is non empty Relation-like set

AllSymbolsOf C is non empty non trivial non finite non empty-membered set
the U1 of C is set
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (C) is non empty Element of bool (bool (C))
bool (C) is non empty set
bool (bool (C)) is non empty set
Funcs ((bool (C)),(bool (C))) is non empty functional FUNCTION_DOMAIN of bool (C), bool (C)
bool (Funcs ((bool (C)),(bool (C)))) is non empty set
[:(bool (C)),(bool (C)):] is non empty Relation-like set
bool [:(bool (C)),(bool (C)):] is non empty set
phi is functional Element of bool (Funcs ((bool (C)),(bool (C))))
(C,phi) is Relation-like bool (C) -defined bool (C) -valued Function-like total quasi_total Element of Funcs ((bool (C)),(bool (C)))
dom (C,phi) is Element of bool (bool (C))
bool (bool (C)) is non empty set
proj2 (C,phi) is set
iter ((C,phi),X) is Relation-like Function-like set
proj1 (iter ((C,phi),X)) is set
(dom (C,phi)) \/ (proj2 (C,phi)) is set
S is Relation-like bool (C) -defined bool (C) -valued Function-like total quasi_total Element of Funcs ((bool (C)),(bool (C)))
dom S is Element of bool (bool (C))

proj1 (iter (S,X)) is set
DD is Relation-like (C) Element of bool (C)
FF is (C) set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
(X,C) is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
phi is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set
iter ((X,C),phi) is Relation-like Function-like set
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is V51() V53() eligible Language-like
(C) is non empty Relation-like set

AllSymbolsOf C is non empty non trivial non finite non empty-membered set
the U1 of C is set
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (C) is non empty Element of bool (bool (C))
bool (C) is non empty set
bool (bool (C)) is non empty set
Funcs ((bool (C)),(bool (C))) is non empty functional FUNCTION_DOMAIN of bool (C), bool (C)
bool (Funcs ((bool (C)),(bool (C)))) is non empty set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
(X,C) is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
{ (iter ((X,C),b1)) where b1 is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT : verum } is set
[:(bool (X)),(bool (X)):] is non empty Relation-like bool (X) -defined bool (X) -valued Element of bool [:(bool (X)),(bool (X)):]
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
bool [:(bool (X)),(bool (X)):] is non empty set
bool (bool [:(bool (X)),(bool (X)):]) is non empty set
FF is set
D is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT
iter ((X,C),D) is Relation-like Function-like set
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
bool [:(bool (X)),(bool (X)):] is non empty Element of bool (bool [:(bool (X)),(bool (X)):])
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b1 is b2 -wff } is set
bool () is non empty set
{ } is set
bool (X) is non empty Element of bool (bool (X))
bool (X) is non empty set
bool (bool (X)) is non empty set
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)

[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
C is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
S is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
DD is Relation-like (X) Element of bool (X)
S . DD is Relation-like (X) Element of bool (X)
FF is Relation-like (X) Element of bool (X)
S . FF is Relation-like (X) Element of bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set

AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite non empty-membered set
() * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (() *)
bool (() *) is non empty non trivial non finite non empty-membered set
(() *) typed\ is functional V36() FinSequence-membered Element of bool (() *)
{ b1 where b1 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (() *) \ : ex b2 being V4() V5()