:: MBOOLEAN semantic presentation

{} is empty set
bool {} is non empty set
{{}} is non empty set
union {} is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
i . Y9 is set
A . Y9 is set
bool (A . Y9) is non empty set
X9 . Y9 is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is set
(I,A) . i is set
A . i is set
bool (A . i) is non empty set
A is set
I is set
i is set
I .--> i is Relation-like {I} -defined Function-like one-to-one set
{I} is non empty set
{I} --> i is Relation-like {I} -defined Function-like constant non empty V14({I}) quasi_total M2( bool [:{I},{i}:])
{i} is non empty set
[:{I},{i}:] is non empty set
bool [:{I},{i}:] is non empty set
X9 is Relation-like A -defined Function-like V14(A) set
X9 +* (I .--> i) is Relation-like Function-like set
dom (X9 +* (I .--> i)) is set
dom X9 is set
dom (I .--> i) is set
(dom X9) \/ (dom (I .--> i)) is set
A \/ (dom (I .--> i)) is set
A \/ {I} is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
(I,(A \/ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
bool ((A . X9) \/ (i . X9)) is non empty set
(A \/ i) . X9 is set
bool ((A \/ i) . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A /\ i is Relation-like I -defined Function-like V14(I) set
(I,(A /\ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
(I,(A /\ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) /\ (i . X9) is set
bool ((A . X9) /\ (i . X9)) is non empty set
(A /\ i) . X9 is set
bool ((A /\ i) . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \ i is Relation-like I -defined Function-like V14(I) set
(I,(A \ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
(I,(A \ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \ (i . X9) is set
bool ((A . X9) \ (i . X9)) is non empty set
(A \ i) . X9 is set
bool ((A \ i) . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \+\ i is Relation-like I -defined Function-like V14(I) set
A \ i is Relation-like I -defined Function-like V14(I) set
i \ A is Relation-like I -defined Function-like V14(I) set
(A \ i) \/ (i \ A) is Relation-like I -defined Function-like V14(I) set
(I,(A \+\ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
(I,(A \+\ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \+\ (i . X9) is set
bool ((A . X9) \+\ (i . X9)) is non empty set
(A \+\ i) . X9 is set
bool ((A \+\ i) . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
X9 . Y9 is set
i . Y9 is set
A . Y9 is set
bool (i . Y9) is non empty set
Y9 is set
X9 . Y9 is set
A . Y9 is set
i . Y9 is set
bool (i . Y9) is non empty set
X9 is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
A . X9 is set
i . X9 is set
Y9 is set
X9 .--> Y9 is Relation-like {X9} -defined Function-like one-to-one set
{X9} is non empty set
{X9} --> Y9 is Relation-like {X9} -defined Function-like constant non empty V14({X9}) quasi_total M2( bool [:{X9},{Y9}:])
{Y9} is non empty set
[:{X9},{Y9}:] is non empty set
bool [:{X9},{Y9}:] is non empty set
dom (X9 .--> Y9) is set
([[0]] I) +* (X9 .--> Y9) is Relation-like Function-like set
dom (([[0]] I) +* (X9 .--> Y9)) is set
M is Relation-like I -defined Function-like V14(I) set
M . X9 is set
(X9 .--> Y9) . X9 is set
K1 is set
M . K1 is set
A . K1 is set
([[0]] I) . K1 is set
K1 is set
M . K1 is set
i . K1 is set
([[0]] I) . K1 is set
bool (i . X9) is non empty set
(I,i) . X9 is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
(I,([[0]] I)) is Relation-like non-empty I -defined Function-like V14(I) set
I --> {{}} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{{}}}:])
{{{}}} is non empty set
[:I,{{{}}}:] is set
bool [:I,{{{}}}:] is non empty set
A is set
(I,([[0]] I)) . A is set
([[0]] I) . A is set
bool (([[0]] I) . A) is non empty set
(I --> {{}}) . A is set
I is set
A is set
I --> A is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{A}:])
{A} is non empty set
[:I,{A}:] is set
bool [:I,{A}:] is non empty set
(I,(I --> A)) is Relation-like non-empty I -defined Function-like V14(I) set
bool A is non empty set
I --> (bool A) is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{(bool A)}:])
{(bool A)} is non empty set
[:I,{(bool A)}:] is set
bool [:I,{(bool A)}:] is non empty set
i is set
(I,(I --> A)) . i is set
(I --> A) . i is set
bool ((I --> A) . i) is non empty set
(I --> (bool A)) . i is set
I is set
A is set
{A} is non empty set
I --> {A} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{A}}:])
{{A}} is non empty set
[:I,{{A}}:] is set
bool [:I,{{A}}:] is non empty set
(I,(I --> {A})) is Relation-like non-empty I -defined Function-like V14(I) set
{{},{A}} is non empty set
I --> {{},{A}} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{{},{A}}}:])
{{{},{A}}} is non empty set
[:I,{{{},{A}}}:] is set
bool [:I,{{{},{A}}}:] is non empty set
i is set
(I,(I --> {A})) . i is set
(I --> {A}) . i is set
bool ((I --> {A}) . i) is non empty set
bool {A} is non empty set
(I --> {{},{A}}) . i is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
A is Relation-like I -defined Function-like V14(I) set
i is set
([[0]] I) . i is set
A . i is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
(I,A) . X9 is set
(I,i) . X9 is set
A . X9 is set
i . X9 is set
bool (A . X9) is non empty set
bool (i . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
(I,A) \/ (I,i) is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
((I,A) \/ (I,i)) . X9 is set
(I,(A \/ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
bool ((A . X9) \/ (i . X9)) is non empty set
(I,A) . X9 is set
(I,i) . X9 is set
((I,A) . X9) \/ ((I,i) . X9) is set
bool (A . X9) is non empty set
(bool (A . X9)) \/ ((I,i) . X9) is non empty set
bool (i . X9) is non empty set
(bool (A . X9)) \/ (bool (i . X9)) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
(I,A) \/ (I,i) is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
bool ((A . X9) \/ (i . X9)) is non empty set
((I,A) \/ (I,i)) . X9 is set
(I,A) . X9 is set
(I,i) . X9 is set
((I,A) . X9) \/ ((I,i) . X9) is set
bool (i . X9) is non empty set
((I,A) . X9) \/ (bool (i . X9)) is non empty set
bool (A . X9) is non empty set
(bool (A . X9)) \/ (bool (i . X9)) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A /\ i is Relation-like I -defined Function-like V14(I) set
(I,(A /\ i)) is Relation-like non-empty I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
(I,A) /\ (I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A /\ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) /\ (i . X9) is set
bool ((A . X9) /\ (i . X9)) is non empty set
bool (A . X9) is non empty set
bool (i . X9) is non empty set
(bool (A . X9)) /\ (bool (i . X9)) is set
(I,i) . X9 is set
(bool (A . X9)) /\ ((I,i) . X9) is set
(I,A) . X9 is set
((I,A) . X9) /\ ((I,i) . X9) is set
((I,A) /\ (I,i)) . X9 is set
I is set
I --> {{}} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{{}}}:])
{{{}}} is non empty set
[:I,{{{}}}:] is set
bool [:I,{{{}}}:] is non empty set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \ i is Relation-like I -defined Function-like V14(I) set
(I,(A \ i)) is Relation-like non-empty I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
(I,A) \ (I,i) is Relation-like I -defined Function-like V14(I) set
(I --> {{}}) \/ ((I,A) \ (I,i)) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A \ i)) . X9 is set
((I --> {{}}) \/ ((I,A) \ (I,i))) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \ (i . X9) is set
bool ((A . X9) \ (i . X9)) is non empty set
(I --> {{}}) . X9 is set
((I,A) \ (I,i)) . X9 is set
((I --> {{}}) . X9) \/ (((I,A) \ (I,i)) . X9) is set
{{}} \/ (((I,A) \ (I,i)) . X9) is non empty set
(I,A) . X9 is set
(I,i) . X9 is set
((I,A) . X9) \ ((I,i) . X9) is set
{{}} \/ (((I,A) . X9) \ ((I,i) . X9)) is non empty set
bool (A . X9) is non empty set
(bool (A . X9)) \ ((I,i) . X9) is set
{{}} \/ ((bool (A . X9)) \ ((I,i) . X9)) is non empty set
bool (i . X9) is non empty set
(bool (A . X9)) \ (bool (i . X9)) is set
{{}} \/ ((bool (A . X9)) \ (bool (i . X9))) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
i \ X9 is Relation-like I -defined Function-like V14(I) set
(I,(i \ X9)) is Relation-like non-empty I -defined Function-like V14(I) set
Y9 is set
A . Y9 is set
i . Y9 is set
(I,(i \ X9)) . Y9 is set
X9 . Y9 is set
(i . Y9) \ (X9 . Y9) is set
bool ((i . Y9) \ (X9 . Y9)) is non empty set
Y9 is set
A . Y9 is set
X9 . Y9 is set
(I,(i \ X9)) . Y9 is set
i . Y9 is set
(i . Y9) \ (X9 . Y9) is set
bool ((i . Y9) \ (X9 . Y9)) is non empty set
Y9 is set
A . Y9 is set
(i \ X9) . Y9 is set
i . Y9 is set
X9 . Y9 is set
(i . Y9) \ (X9 . Y9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \ i is Relation-like I -defined Function-like V14(I) set
(I,(A \ i)) is Relation-like non-empty I -defined Function-like V14(I) set
i \ A is Relation-like I -defined Function-like V14(I) set
(I,(i \ A)) is Relation-like non-empty I -defined Function-like V14(I) set
(I,(A \ i)) \/ (I,(i \ A)) is Relation-like I -defined Function-like V14(I) set
A \+\ i is Relation-like I -defined Function-like V14(I) set
(A \ i) \/ (i \ A) is Relation-like I -defined Function-like V14(I) set
(I,(A \+\ i)) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
((I,(A \ i)) \/ (I,(i \ A))) . X9 is set
(I,(A \+\ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \+\ (i . X9) is set
bool ((A . X9) \+\ (i . X9)) is non empty set
(I,(A \ i)) . X9 is set
(I,(i \ A)) . X9 is set
((I,(A \ i)) . X9) \/ ((I,(i \ A)) . X9) is set
(A . X9) \ (i . X9) is set
bool ((A . X9) \ (i . X9)) is non empty set
(bool ((A . X9) \ (i . X9))) \/ ((I,(i \ A)) . X9) is non empty set
(i . X9) \ (A . X9) is set
bool ((i . X9) \ (A . X9)) is non empty set
(bool ((A . X9) \ (i . X9))) \/ (bool ((i . X9) \ (A . X9))) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
i \+\ X9 is Relation-like I -defined Function-like V14(I) set
i \ X9 is Relation-like I -defined Function-like V14(I) set
X9 \ i is Relation-like I -defined Function-like V14(I) set
(i \ X9) \/ (X9 \ i) is Relation-like I -defined Function-like V14(I) set
i \/ X9 is Relation-like I -defined Function-like V14(I) set
i /\ X9 is Relation-like I -defined Function-like V14(I) set
(I,(i \+\ X9)) is Relation-like non-empty I -defined Function-like V14(I) set
Y9 is set
A . Y9 is set
(i \/ X9) . Y9 is set
(I,(i \+\ X9)) . Y9 is set
i . Y9 is set
X9 . Y9 is set
(i . Y9) \+\ (X9 . Y9) is set
bool ((i . Y9) \+\ (X9 . Y9)) is non empty set
(i . Y9) \/ (X9 . Y9) is set
Y9 is set
A . Y9 is set
(i /\ X9) . Y9 is set
(I,(i \+\ X9)) . Y9 is set
i . Y9 is set
X9 . Y9 is set
(i . Y9) \+\ (X9 . Y9) is set
bool ((i . Y9) \+\ (X9 . Y9)) is non empty set
(i . Y9) /\ (X9 . Y9) is set
Y9 is set
A . Y9 is set
(i \+\ X9) . Y9 is set
(i /\ X9) . Y9 is set
i . Y9 is set
X9 . Y9 is set
(i . Y9) /\ (X9 . Y9) is set
(i \/ X9) . Y9 is set
(i . Y9) \/ (X9 . Y9) is set
(i . Y9) \+\ (X9 . Y9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
A /\ X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
(A /\ X9) . Y9 is set
i . Y9 is set
A . Y9 is set
X9 . Y9 is set
(A . Y9) /\ (X9 . Y9) is set
Y9 is set
(A /\ X9) . Y9 is set
i . Y9 is set
X9 . Y9 is set
A . Y9 is set
(A . Y9) /\ (X9 . Y9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
A \ X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
(A \ X9) . Y9 is set
i . Y9 is set
A . Y9 is set
X9 . Y9 is set
(A . Y9) \ (X9 . Y9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
A \+\ X9 is Relation-like I -defined Function-like V14(I) set
A \ X9 is Relation-like I -defined Function-like V14(I) set
X9 \ A is Relation-like I -defined Function-like V14(I) set
(A \ X9) \/ (X9 \ A) is Relation-like I -defined Function-like V14(I) set
Y9 is set
(A \+\ X9) . Y9 is set
i . Y9 is set
A . Y9 is set
X9 . Y9 is set
(A . Y9) \+\ (X9 . Y9) is set
bool (i . Y9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
[|A,i|] is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like non-empty I -defined Function-like V14(I) set
(I,(I,(A \/ i))) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
[|A,i|] . X9 is set
(I,(I,(A \/ i))) . X9 is set
A . X9 is set
i . X9 is set
[:(A . X9),(i . X9):] is set
(I,(A \/ i)) . X9 is set
bool ((I,(A \/ i)) . X9) is non empty set
(A . X9) \/ (i . X9) is set
bool ((A . X9) \/ (i . X9)) is non empty set
bool (bool ((A . X9) \/ (i . X9))) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
A . X9 is set
(I,i) . X9 is set
i . X9 is set
bool (i . X9) is non empty set
X9 is set
A . X9 is set
i . X9 is set
(I,i) . X9 is set
bool (i . X9) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(Funcs) (A,i) is Relation-like I -defined Function-like V14(I) set
[|A,i|] is Relation-like I -defined Function-like V14(I) set
(I,[|A,i|]) is Relation-like non-empty I -defined Function-like V14(I) set
X9 is set
((Funcs) (A,i)) . X9 is set
(I,[|A,i|]) . X9 is set
A . X9 is set
i . X9 is set
Funcs ((A . X9),(i . X9)) is set
[|A,i|] . X9 is set
bool ([|A,i|] . X9) is non empty set
[:(A . X9),(i . X9):] is set
bool [:(A . X9),(i . X9):] is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
i . Y9 is set
A . Y9 is set
union (A . Y9) is set
X9 . Y9 is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
(I,([[0]] I)) is Relation-like I -defined Function-like V14(I) set
A is set
(I,([[0]] I)) . A is set
([[0]] I) . A is set
union (([[0]] I) . A) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A \/ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
union ((A . X9) \/ (i . X9)) is set
(A \/ i) . X9 is set
union ((A \/ i) . X9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A /\ i is Relation-like I -defined Function-like V14(I) set
(I,(A /\ i)) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A /\ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) /\ (i . X9) is set
union ((A . X9) /\ (i . X9)) is set
(A /\ i) . X9 is set
union ((A /\ i) . X9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
A . X9 is set
i . X9 is set
(I,i) . X9 is set
union (i . X9) is set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
A . Y9 is set
X9 . Y9 is set
Y9 is set
X9 . Y9 is set
i . Y9 is set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
A . Y9 is set
(I,i) . Y9 is set
X9 . Y9 is set
i . Y9 is set
union (i . Y9) is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
(I,([[0]] I)) is Relation-like empty-yielding I -defined Function-like V14(I) set
A is set
(I,([[0]] I)) . A is set
([[0]] I) . A is set
union (([[0]] I) . A) is set
I is set
A is set
I --> A is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{A}:])
{A} is non empty set
[:I,{A}:] is set
bool [:I,{A}:] is non empty set
(I,(I --> A)) is Relation-like I -defined Function-like V14(I) set
union A is set
I --> (union A) is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{(union A)}:])
{(union A)} is non empty set
[:I,{(union A)}:] is set
bool [:I,{(union A)}:] is non empty set
i is set
(I,(I --> A)) . i is set
(I --> A) . i is set
union ((I --> A) . i) is set
(I --> (union A)) . i is set
I is set
A is set
{A} is non empty set
I --> {A} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{A}}:])
{{A}} is non empty set
[:I,{{A}}:] is set
bool [:I,{{A}}:] is non empty set
(I,(I --> {A})) is Relation-like I -defined Function-like V14(I) set
I --> A is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{A}:])
[:I,{A}:] is set
bool [:I,{A}:] is non empty set
i is set
(I,(I --> {A})) . i is set
(I --> {A}) . i is set
union ((I --> {A}) . i) is set
union {A} is set
(I --> A) . i is set
I is set
A is set
{A} is non empty set
i is set
{i} is non empty set
{{A},{i}} is non empty set
I --> {{A},{i}} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{{A},{i}}}:])
{{{A},{i}}} is non empty set
[:I,{{{A},{i}}}:] is set
bool [:I,{{{A},{i}}}:] is non empty set
(I,(I --> {{A},{i}})) is Relation-like I -defined Function-like V14(I) set
{A,i} is non empty set
I --> {A,i} is Relation-like non-empty I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{A,i}}:])
{{A,i}} is non empty set
[:I,{{A,i}}:] is set
bool [:I,{{A,i}}:] is non empty set
X9 is set
(I,(I --> {{A},{i}})) . X9 is set
(I --> {{A},{i}}) . X9 is set
union ((I --> {{A},{i}}) . X9) is set
union {{A},{i}} is set
(I --> {A,i}) . X9 is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
A . X9 is set
(I,i) . X9 is set
i . X9 is set
union (i . X9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,A) . X9 is set
(I,i) . X9 is set
A . X9 is set
i . X9 is set
union (A . X9) is set
union (i . X9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
(I,(A \/ i)) is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
(I,A) \/ (I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A \/ i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
union ((A . X9) \/ (i . X9)) is set
union (A . X9) is set
union (i . X9) is set
(union (A . X9)) \/ (union (i . X9)) is set
(I,A) . X9 is set
((I,A) . X9) \/ (union (i . X9)) is set
(I,i) . X9 is set
((I,A) . X9) \/ ((I,i) . X9) is set
((I,A) \/ (I,i)) . X9 is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A /\ i is Relation-like I -defined Function-like V14(I) set
(I,(A /\ i)) is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
(I,A) /\ (I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,(A /\ i)) . X9 is set
((I,A) /\ (I,i)) . X9 is set
A . X9 is set
i . X9 is set
(A . X9) /\ (i . X9) is set
union ((A . X9) /\ (i . X9)) is set
(I,A) . X9 is set
(I,i) . X9 is set
((I,A) . X9) /\ ((I,i) . X9) is set
union (A . X9) is set
(union (A . X9)) /\ ((I,i) . X9) is set
union (i . X9) is set
(union (A . X9)) /\ (union (i . X9)) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like non-empty I -defined Function-like V14(I) set
(I,(I,A)) is Relation-like I -defined Function-like V14(I) set
i is set
(I,(I,A)) . i is set
(I,A) . i is set
union ((I,A) . i) is set
A . i is set
bool (A . i) is non empty set
union (bool (A . i)) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
(I,(I,A)) is Relation-like non-empty I -defined Function-like V14(I) set
i is set
A . i is set
(I,(I,A)) . i is set
(I,A) . i is set
bool ((I,A) . i) is non empty set
union (A . i) is set
bool (union (A . i)) is non empty set
I is set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like I -defined Function-like V14(I) set
Y9 is set
X9 . Y9 is set
i . Y9 is set
(I,A) . Y9 is set
A . Y9 is set
union (A . Y9) is set
I is set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like non-empty I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
(I,i) . X9 is set
A . X9 is set
i . X9 is set
Y9 is Relation-like I -defined Function-like V14(I) set
M is set
X9 .--> M is Relation-like {X9} -defined Function-like one-to-one set
{X9} is non empty set
{X9} --> M is Relation-like {X9} -defined Function-like constant non empty V14({X9}) quasi_total M2( bool [:{X9},{M}:])
{M} is non empty set
[:{X9},{M}:] is non empty set
bool [:{X9},{M}:] is non empty set
Y9 +* (X9 .--> M) is Relation-like Function-like set
dom (Y9 +* (X9 .--> M)) is set
dom (X9 .--> M) is set
K1 is Relation-like I -defined Function-like V14(I) set
K1 . X9 is set
(X9 .--> M) . X9 is set
K2 is set
K1 . K2 is set
i . K2 is set
Y9 . K2 is set
union (i . X9) is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like non-empty I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
(I,i) /\ A is Relation-like I -defined Function-like V14(I) set
X9 is set
i . X9 is set
A . X9 is set
Y9 is Relation-like I -defined Function-like V14(I) set
M is set
X9 .--> M is Relation-like {X9} -defined Function-like one-to-one set
{X9} is non empty set
{X9} --> M is Relation-like {X9} -defined Function-like constant non empty V14({X9}) quasi_total M2( bool [:{X9},{M}:])
{M} is non empty set
[:{X9},{M}:] is non empty set
bool [:{X9},{M}:] is non empty set
Y9 +* (X9 .--> M) is Relation-like Function-like set
dom (Y9 +* (X9 .--> M)) is set
dom (X9 .--> M) is set
K1 is Relation-like I -defined Function-like V14(I) set
K1 . X9 is set
(X9 .--> M) . X9 is set
K2 is set
K1 . K2 is set
i . K2 is set
Y9 . K2 is set
K1 /\ A is Relation-like I -defined Function-like V14(I) set
(K1 . X9) /\ (A . X9) is set
([[0]] I) . X9 is set
M /\ (A . X9) is set
union (i . X9) is set
(union (i . X9)) /\ (A . X9) is set
(I,i) . X9 is set
((I,i) . X9) /\ (A . X9) is set
((I,i) /\ A) . X9 is set
([[0]] I) . X9 is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
A is Relation-like I -defined Function-like V14(I) set
i is Relation-like I -defined Function-like V14(I) set
A \/ i is Relation-like I -defined Function-like V14(I) set
A /\ i is Relation-like I -defined Function-like V14(I) set
(I,(A /\ i)) is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
(I,i) is Relation-like I -defined Function-like V14(I) set
(I,A) /\ (I,i) is Relation-like I -defined Function-like V14(I) set
X9 is set
A . X9 is set
i . X9 is set
(A . X9) \/ (i . X9) is set
Y9 is Relation-like I -defined Function-like V14(I) set
{X9} is non empty set
M is set
K1 is set
X9 .--> M is Relation-like {X9} -defined Function-like one-to-one set
{X9} --> M is Relation-like {X9} -defined Function-like constant non empty V14({X9}) quasi_total M2( bool [:{X9},{M}:])
{M} is non empty set
[:{X9},{M}:] is non empty set
bool [:{X9},{M}:] is non empty set
Y9 +* (X9 .--> M) is Relation-like Function-like set
dom (Y9 +* (X9 .--> M)) is set
X9 .--> K1 is Relation-like {X9} -defined Function-like one-to-one set
{X9} --> K1 is Relation-like {X9} -defined Function-like constant non empty V14({X9}) quasi_total M2( bool [:{X9},{K1}:])
{K1} is non empty set
[:{X9},{K1}:] is non empty set
bool [:{X9},{K1}:] is non empty set
Y9 +* (X9 .--> K1) is Relation-like Function-like set
dom (Y9 +* (X9 .--> K1)) is set
dom (X9 .--> K1) is set
j is Relation-like I -defined Function-like V14(I) set
j . X9 is set
(X9 .--> K1) . X9 is set
j is set
j . j is set
(A \/ i) . j is set
Y9 . j is set
dom (X9 .--> M) is set
K2 is Relation-like I -defined Function-like V14(I) set
K2 . X9 is set
(X9 .--> M) . X9 is set
j is set
K2 . j is set
(A \/ i) . j is set
Y9 . j is set
K2 /\ j is Relation-like I -defined Function-like V14(I) set
(K2 /\ j) . X9 is set
M /\ K1 is set
(A . X9) /\ (i . X9) is set
union ((A . X9) /\ (i . X9)) is set
union (A . X9) is set
union (i . X9) is set
(union (A . X9)) /\ (union (i . X9)) is set
(I,A) . X9 is set
((I,A) . X9) /\ (union (i . X9)) is set
(I,i) . X9 is set
((I,A) . X9) /\ ((I,i) . X9) is set
((I,A) /\ (I,i)) . X9 is set
(I,(A /\ i)) . X9 is set
I is set
[[0]] I is Relation-like I -defined Function-like V14(I) set
I --> {} is Relation-like I -defined Function-like constant V14(I) quasi_total M2( bool [:I,{{}}:])
[:I,{{}}:] is set
bool [:I,{{}}:] is non empty set
i is Relation-like I -defined Function-like V14(I) set
A is Relation-like I -defined Function-like V14(I) set
(I,A) is Relation-like I -defined Function-like V14(I) set
X9 is Relation-like non-empty I -defined Function-like V14(I) set
A \/ X9 is Relation-like I -defined Function-like V14(I) set
(I,(A \/ X9)) is Relation-like I -defined Function-like V14(I) set
Y9 is set
i . Y9 is set
(I,A) . Y9 is set
X9 . Y9 is set
M is Relation-like I -defined Function-like V14(I) set
K1 is set
Y9 .--> K1 is Relation-like {Y9} -defined Function-like one-to-one set
{Y9} is non empty set
{Y9} --> K1 is Relation-like {Y9} -defined Function-like constant non empty V14({Y9}) quasi_total M2( bool [:{Y9},{K1}:])
{K1} is non empty set
[:{Y9},{K1}:] is non empty set
bool [:{Y9},{K1}:] is non empty set
M +* (Y9 .--> K1) is Relation-like Function-like set
dom (M +* (Y9 .--> K1)) is set
dom (Y9 .--> K1) is set
K2 is Relation-like I -defined Function-like V14(I) set
K2 . Y9 is set
(Y9 .--> K1) . Y9 is set
j is set
K2 . j is set
X9 . j is set
M . j is set
K2 /\ i is Relation-like I -defined Function-like V14(I) set
(K2 /\ i) . Y9 is set
K1 /\ (i . Y9) is set
(I,(A \/ X9)) . Y9 is set
A . Y9 is set
(A . Y9) \/ (X9 . Y9) is set
union ((A . Y9) \/ (X9 . Y9)) is set
union (A . Y9) is set
I is set
A is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set
(I,A) is Relation-like I -defined Function-like V14(I) set
i is set
(I,A) . i is set
A . i is set
dom A is set
rng A is set
X9 is set
Y9 is set
M is Relation-like I -defined Function-like V14(I) set
i .--> Y9 is Relation-like {i} -defined Function-like one-to-one set
{i} is non empty set
{i} --> Y9 is Relation-like {i} -defined Function-like constant non empty V14({i}) quasi_total M2( bool [:{i},{Y9}:])
{Y9} is non empty set
[:{i},{Y9}:] is non empty set
bool [:{i},{Y9}:] is non empty set
M +* (i .--> Y9) is Relation-like Function-like set
dom (M +* (i .--> Y9)) is set
i .--> X9 is Relation-like {i} -defined Function-like one-to-one set
{i} --> X9 is Relation-like {i} -defined Function-like constant non empty V14({i}) quasi_total M2( bool [:{i},{X9}:])
{X9} is non empty set
[:{i},{X9}:] is non empty set
bool [:{i},{X9}:] is non empty set
M +* (i .--> X9) is Relation-like Function-like set
dom (M +* (i .--> X9)) is set
dom (i .--> Y9) is set
K2 is Relation-like I -defined Function-like V14(I) set
K2 . i is set
(i .--> Y9) . i is set
j is set
K2 . j is set
A . j is set
M . j is set
dom (i .--> X9) is set
K1 is Relation-like I -defined Function-like V14(I) set
K1 . i is set
(i .--> X9) . i is set
j is set
K1 . j is set
A . j is set
M . j is set
union (A . i) is set