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