:: MBOOLEAN semantic presentation

bool {} is non empty set
is non empty set

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

(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} is non empty set

{i} is non empty set
[:{I},{i}:] is non empty set
bool [:{I},{i}:] is non empty 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

(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

(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

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

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

[:I,:] is set
bool [:I,:] is non empty set
A . X9 is set
i . X9 is set
Y9 is 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
() +* (X9 .--> Y9) is Relation-like Function-like set
dom (() +* (X9 .--> Y9)) is set

M . X9 is set
(X9 .--> Y9) . X9 is set
K1 is set
M . K1 is set
A . K1 is set
() . K1 is set
K1 is set
M . K1 is set
i . K1 is set
() . K1 is set
bool (i . X9) is non empty set
(I,i) . X9 is set
I is set

[:I,:] is set
bool [:I,:] is non empty set
(I,()) is Relation-like non-empty I -defined Function-like V14(I) set

is non empty set
is set
bool is non empty set
A is set
(I,()) . A is set
() . A is set
bool (() . A) is non empty set
() . A is set
I is set
A is set

{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

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

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

{{{},{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

[:I,:] is set
bool [:I,:] is non empty set

i is set
() . i is set
A . i is set
I is 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

(I,A) \/ (I,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

(I,A) \/ (I,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

(I,(A /\ 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

is non empty set
is set
bool is non empty set

(I,(A \ 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,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
bool ((A . X9) \ (i . X9)) is non empty set
() . X9 is set
((I,A) \ (I,i)) . X9 is set
(() . 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

(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

(I,(A \ i)) is Relation-like non-empty 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) \/ (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

(i \ X9) \/ (X9 \ i) 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

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

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

(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

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

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

Y9 is set
i . Y9 is set
A . Y9 is set
union (A . Y9) is set
X9 . Y9 is set
I is set

[:I,:] is set
bool [:I,:] is non empty set
(I,()) is Relation-like I -defined Function-like V14(I) set
A is set
(I,()) . A is set
() . A is set
union (() . A) is set
I is 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

(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

(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

Y9 is set
A . Y9 is set
X9 . Y9 is set
Y9 is set
X9 . Y9 is set
i . Y9 is 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

[:I,:] is set
bool [:I,:] is non empty set
(I,()) is Relation-like empty-yielding I -defined Function-like V14(I) set
A is set
(I,()) . A is set
() . A is set
union (() . A) is set
I is set
A is set

{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

{()} is non empty set
[:I,{()}:] is set
bool [:I,{()}:] 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 --> ()) . i is set
I is set
A is set
{A} is non empty set

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

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

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

(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

(I,A) 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

(I,A) 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

(I,A) 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

(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

(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

(I,A) 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

(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

M is set

{X9} is non empty set

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

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

M is set

{X9} is non empty set

{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 . X9 is set
(X9 .--> M) . X9 is set
K2 is set
K1 . K2 is set
i . K2 is set
Y9 . K2 is set

(K1 . X9) /\ (A . X9) is set
() . 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
() . X9 is set
I is set

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

{X9} is non empty set
M is set
K1 is set

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

[:I,:] is set
bool [:I,:] is non empty set

(I,A) 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

K1 is 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 . 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) . 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

(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

{i} is non empty set

{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

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