:: PZFMISC1 semantic presentation

dom {} is set
rng {} is set
I is set
A is set
B is set

{A} is non empty finite set

{B} is non empty finite set
[:{A},{B}:] is finite set
bool [:{A},{B}:] is finite V29() set

B +* (A .--> B) is Relation-like Function-like set
dom (B +* (A .--> B)) is set
dom B is set
dom (A .--> B) is finite set
(dom B) \/ (dom (A .--> B)) is set
I \/ (dom (A .--> B)) is set
I \/ {A} is non empty set

I is set

B is set
A . B is set
I is set

y is set
B . y is set
A . y is set
{(A . y)} is non empty finite set
B . y is set
I is set

(I,A) is Relation-like I -defined Function-like V14(I) set
B is set
(I,A) . B is set
A . B is set
{(A . B)} is non empty finite set
B is set
(I,A) . B is set
A . B is set
{(A . B)} is non empty finite set
I is set

X is set
B . X is set
A . X is set
B . X is set
{(A . X),(B . X)} is non empty finite set
y . X is set

Y is set
B . Y is set
X . Y is set
y . Y is set
{(X . Y),(y . Y)} is non empty finite set
I is set

(I,A,B) is Relation-like I -defined Function-like V14(I) set
B is set
(I,A,B) . B is set
A . B is set
B . B is set
{(A . B),(B . B)} is non empty finite set
B is set
(I,A,B) . B is set
A . B is set
B . B is set
{(A . B),(B . B)} is non empty finite set
I is set

y is set
B . y is set
A . y is set
B . y is set
{(B . y)} is non empty finite set
y is set
B . y is set
A . y is set
B . y is set
{(B . y)} is non empty finite set
B is set
y is set
A . B is set
B . B is set

{B} is non empty finite set

{y} is non empty finite set
[:{B},{y}:] is finite set
bool [:{B},{y}:] is finite V29() set
dom (B .--> y) is finite set
B +* (B .--> y) is Relation-like Function-like set
dom (B +* (B .--> y)) is set

X . B is set
(B .--> y) . B is set
Y is set
X . Y is set
A . Y is set
B . Y is set
{(B . B)} is non empty finite set
(I,B) . B is finite set
I is set

y is set
X is set
A . y is set
B . y is set
B . y is set

{y} is non empty finite set

{X} is non empty finite set
[:{y},{X}:] is finite set
bool [:{y},{X}:] is finite V29() set
dom (y .--> X) is finite set
B +* (y .--> X) is Relation-like Function-like set
dom (B +* (y .--> X)) is set

Y . y is set
(y .--> X) . y is set
i is set
Y . i is set
A . i is set
B . i is set
{(B . y),(B . y)} is non empty finite set
(I,B,B) . y is finite set
I is set

X is set
y . X is set
A . X is set
B . X is set
B . X is set
{(B . X),(B . X)} is non empty finite set
I is set

B is set
A . B is set
(I,B) . B is finite set
B . B is set
{(B . B)} is non empty finite set
I is set

B is set
A . B is set
(I,A) . B is finite set
{(A . B)} is non empty finite set
I is set

y is set
A . y is set
(I,B,B) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
y is set
A . y is set
(I,B,B) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
I is set

(I,A) \/ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set
((I,A) \/ (I,B)) . B is set
(I,A) . B is finite set
(I,B) . B is finite set
((I,A) . B) \/ ((I,B) . B) is finite set
B . B is set
{(B . B)} is non empty finite set
((I,A) . B) \/ {(B . B)} is non empty finite set
A . B is set
{(A . B)} is non empty finite set
{(A . B)} \/ {(B . B)} is non empty finite set
{(A . B),(B . B)} is non empty finite set
(I,A,B) . B is finite set
I is set

B is set
(I,A,A) . B is finite set
A . B is set
{(A . B),(A . B)} is non empty finite set
{(A . B)} is non empty finite set
(I,A) . B is finite set
I is set

B is set
(I,A) . B is finite set
(I,B) . B is finite set
B . B is set
{(B . B)} is non empty finite set
A . B is set
{(A . B)} is non empty finite set
I is set

B is set
A . B is set
{(A . B)} is non empty finite set
(I,A) . B is finite set
B . B is set
{(B . B)} is non empty finite set
I is set

y is set
A . y is set
{(A . y)} is non empty finite set
(I,A) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
y is set
A . y is set
{(A . y)} is non empty finite set
(I,A) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
I is set

y is set
A . y is set
{(A . y)} is non empty finite set
(I,A) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
I is set

B is set
(I,A) . B is finite set
(I,A,B) . B is finite set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(A . B),(B . B)} is non empty finite set
B is set
(I,B) . B is finite set
(I,A,B) . B is finite set
B . B is set
{(B . B)} is non empty finite set
A . B is set
{(A . B),(B . B)} is non empty finite set
I is set

(I,A) \/ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
{(A . B)} \/ {(B . B)} is non empty finite set
(I,B) . B is finite set
{(A . B)} \/ ((I,B) . B) is non empty finite set
(I,A) . B is finite set
((I,A) . B) \/ ((I,B) . B) is finite set
((I,A) \/ (I,B)) . B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
{(A . B)} \/ {(B . B)} is non empty finite set
(I,B) . B is finite set
{(A . B)} \/ ((I,B) . B) is non empty finite set
(I,A) . B is finite set
((I,A) . B) \/ ((I,B) . B) is finite set
((I,A) \/ (I,B)) . B is set
I is set

(I,A) \/ (I,A,B) is Relation-like I -defined Function-like V14(I) set
B is set
((I,A) \/ (I,A,B)) . B is set
(I,A) . B is finite set
(I,A,B) . B is finite set
((I,A) . B) \/ ((I,A,B) . B) is finite set
A . B is set
{(A . B)} is non empty finite set
{(A . B)} \/ ((I,A,B) . B) is non empty finite set
B . B is set
{(A . B),(B . B)} is non empty finite set
{(A . B)} \/ {(A . B),(B . B)} is non empty finite set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) /\ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
y is set
A . y is set
{(A . y)} is non empty finite set
B . y is set
{(B . y)} is non empty finite set
{(A . y)} /\ {(B . y)} is finite set
(I,A) . y is finite set
((I,A) . y) /\ {(B . y)} is finite set
(I,B) . y is finite set
((I,A) . y) /\ ((I,B) . y) is finite set
((I,A) /\ (I,B)) . y is set
B is set
A . B is set
B . B is set
I is set

(I,A) /\ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
{(A . B)} /\ {(B . B)} is finite set
(I,B) . B is finite set
{(A . B)} /\ ((I,B) . B) is finite set
(I,A) . B is finite set
((I,A) . B) /\ ((I,B) . B) is finite set
((I,A) /\ (I,B)) . B is set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
{(A . B)} /\ {(B . B)} is finite set
(I,B) . B is finite set
{(A . B)} /\ ((I,B) . B) is finite set
(I,A) . B is finite set
((I,A) . B) /\ ((I,B) . B) is finite set
((I,A) /\ (I,B)) . B is set
I is set

(I,A) /\ (I,A,B) is Relation-like I -defined Function-like V14(I) set

(I,B) /\ (I,A,B) is Relation-like I -defined Function-like V14(I) set
B is set
((I,A) /\ (I,A,B)) . B is set
(I,A) . B is finite set
(I,A,B) . B is finite set
((I,A) . B) /\ ((I,A,B) . B) is finite set
A . B is set
{(A . B)} is non empty finite set
{(A . B)} /\ ((I,A,B) . B) is finite set
B . B is set
{(A . B),(B . B)} is non empty finite set
{(A . B)} /\ {(A . B),(B . B)} is finite set
B is set
((I,B) /\ (I,A,B)) . B is set
(I,B) . B is finite set
(I,A,B) . B is finite set
((I,B) . B) /\ ((I,A,B) . B) is finite set
B . B is set
{(B . B)} is non empty finite set
{(B . B)} /\ ((I,A,B) . B) is finite set
A . B is set
{(A . B),(B . B)} is non empty finite set
{(B . B)} /\ {(A . B),(B . B)} is finite set
I is set

(I,A) \ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
y is set
A . y is set
{(A . y)} is non empty finite set
B . y is set
{(B . y)} is non empty finite set
{(A . y)} \ {(B . y)} is finite set
(I,A) . y is finite set
((I,A) . y) \ {(B . y)} is finite set
(I,B) . y is finite set
((I,A) . y) \ ((I,B) . y) is finite set
((I,A) \ (I,B)) . y is set
B is set
A . B is set
B . B is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) \ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
{(A . B)} \ {(B . B)} is finite set
(I,A) . B is finite set
((I,A) . B) \ {(B . B)} is finite set
(I,B) . B is finite set
((I,A) . B) \ ((I,B) . B) is finite set
((I,A) \ (I,B)) . B is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) \ (I,A,B) is Relation-like I -defined Function-like V14(I) set

(I,B) \ (I,A,B) is Relation-like I -defined Function-like V14(I) set
B is set
((I,A) \ (I,A,B)) . B is set
(I,A) . B is finite set
(I,A,B) . B is finite set
((I,A) . B) \ ((I,A,B) . B) is finite set
A . B is set
{(A . B)} is non empty finite set
{(A . B)} \ ((I,A,B) . B) is finite set
B . B is set
{(A . B),(B . B)} is non empty finite set
{(A . B)} \ {(A . B),(B . B)} is finite set
() . B is set
B is set
((I,B) \ (I,A,B)) . B is set
(I,B) . B is finite set
(I,A,B) . B is finite set
((I,B) . B) \ ((I,A,B) . B) is finite set
B . B is set
{(B . B)} is non empty finite set
{(B . B)} \ ((I,A,B) . B) is finite set
A . B is set
{(A . B),(B . B)} is non empty finite set
{(B . B)} \ {(A . B),(B . B)} is finite set
() . B is set
I is set

B is set
(I,A) . B is finite set
(I,B) . B is finite set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(B . B)} is non empty finite set
I is set

y is set
(I,A,B) . y is finite set
(I,B) . y is finite set
B . y is set
{(B . y)} is non empty finite set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
y is set
(I,A,B) . y is finite set
(I,B) . y is finite set
B . y is set
{(B . y)} is non empty finite set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
I is set

y is set
(I,A,B) . y is finite set
(I,B) . y is finite set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(B . y)} is non empty finite set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

bool (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) finite-yielding set
B is set
(bool (I,A)) . B is set
(I,A) . B is finite set
bool ((I,A) . B) is finite V29() set
A . B is set
{(A . B)} is non empty finite set
bool {(A . B)} is finite V29() set
{{},{(A . B)}} is non empty finite V29() set
() . B is set
{(() . B),{(A . B)}} is non empty finite set
{(() . B),((I,A) . B)} is non empty finite set
(I,(),(I,A)) . B is finite set
I is set

B is set
(I,A) . B is finite set
(bool A) . B is set
A . B is set
{(A . B)} is non empty finite set
bool (A . B) is set
I is set

union (I,A) is Relation-like I -defined Function-like V14(I) set
B is set
(union (I,A)) . B is set
(I,A) . B is finite set
union ((I,A) . B) is set
A . B is set
{(A . B)} is non empty finite set
union {(A . B)} is set
I is set

(I,(I,A),(I,B)) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set
union (I,(I,A),(I,B)) is Relation-like I -defined Function-like V14(I) set

B is set
(union (I,(I,A),(I,B))) . B is set
(I,(I,A),(I,B)) . B is finite set
union ((I,(I,A),(I,B)) . B) is set
(I,A) . B is finite set
(I,B) . B is finite set
{((I,A) . B),((I,B) . B)} is non empty finite V29() set
union {((I,A) . B),((I,B) . B)} is finite set
A . B is set
{(A . B)} is non empty finite set
{{(A . B)},((I,B) . B)} is non empty finite V29() set
union {{(A . B)},((I,B) . B)} is finite set
B . B is set
{(B . B)} is non empty finite set
{{(A . B)},{(B . B)}} is non empty finite V29() set
union {{(A . B)},{(B . B)}} is finite set
{(A . B),(B . B)} is non empty finite set
(I,A,B) . B is finite set
I is set

union (I,A,B) is Relation-like I -defined Function-like V14(I) set

B is set
(union (I,A,B)) . B is set
(I,A,B) . B is finite set
union ((I,A,B) . B) is set
A . B is set
B . B is set
{(A . B),(B . B)} is non empty finite set
union {(A . B),(B . B)} is set
(A . B) \/ (B . B) is set
(A \/ B) . B is set
I is set

B is set
A . B is set
B . B is set
(I,A) . B is finite set
{(A . B)} is non empty finite set
B is set
(I,A) . B is finite set
B . B is set
A . B is set
{(A . B)} is non empty finite set
I is set

y is set
A . y is set
B . y is set
(I,A,B) . y is finite set
B . y is set
{(A . y),(B . y)} is non empty finite set
y is set
B . y is set
B . y is set
(I,A,B) . y is finite set
A . y is set
{(A . y),(B . y)} is non empty finite set
y is set
(I,A,B) . y is finite set
B . y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

y is set
A . y is set
(I,B,B) . y is finite set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
B . y is set
{(B . y)} is non empty finite set
B . y is set
{(B . y),(B . y)} is non empty finite set
B . y is set
{(B . y)} is non empty finite set
B . y is set
{(B . y),(B . y)} is non empty finite set
I is set

B \/ (I,B) is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
(B \/ (I,B)) . y is set
B . y is set
B . y is set
{(B . y)} is non empty finite set
(B . y) \/ {(B . y)} is non empty set
(I,B) . y is finite set
(B . y) \/ ((I,B) . y) is set
B . y is set
B . y is set
{(B . y)} is non empty finite set
(B . y) \/ {(B . y)} is non empty set
(I,B) . y is finite set
(B . y) \/ ((I,B) . y) is set
I is set

A \/ (I,B) is Relation-like I -defined Function-like V14(I) set

y is set
(A \/ (I,B)) . y is set
B . y is set
A . y is set
(I,B) . y is finite set
(A . y) \/ ((I,B) . y) is set
B . y is set
{(B . y)} is non empty finite set
(A . y) \/ {(B . y)} is non empty set
y is set
B . y is set
B . y is set
A . y is set
{(B . y)} is non empty finite set
(A . y) \/ {(B . y)} is non empty set
y is set
A . y is set
B . y is set
B . y is set
{(B . y)} is non empty finite set
(A . y) \/ {(B . y)} is non empty set
y is set
(A \/ (I,B)) . y is set
B . y is set
B . y is set
A . y is set
{(B . y)} is non empty finite set
(A . y) \/ {(B . y)} is non empty set
(I,B) . y is finite set
(A . y) \/ ((I,B) . y) is set
I is set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
B . B is set
{(A . B)} is non empty finite set
{(A . B)} \/ (B . B) is non empty set
(I,A) . B is finite set
((I,A) . B) \/ (B . B) is set
I is set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
B . B is set
((I,A) \/ B) . B is set
(I,A) . B is finite set
((I,A) . B) \/ (B . B) is set
{(A . B)} is non empty finite set
{(A . B)} \/ (B . B) is non empty set
I is set

(I,A,B) \/ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \/ (B . y) is non empty set
(I,A,B) . y is finite set
((I,A,B) . y) \/ (B . y) is set
y is set
B . y is set
B . y is set
A . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \/ (B . y) is non empty set
(I,A,B) . y is finite set
((I,A,B) . y) \/ (B . y) is set
y is set
A . y is set
B . y is set
B . y is set
((I,A,B) \/ B) . y is set
(I,A,B) . y is finite set
((I,A,B) . y) \/ (B . y) is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \/ (B . y) is non empty set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(A . B)} \/ (B . B) is non empty set
(I,A) . B is finite set
((I,A) . B) \/ (B . B) is set
((I,A) \/ B) . B is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A,B) \/ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(A . y),(B . y)} \/ (B . y) is non empty set
(I,A,B) . y is finite set
((I,A,B) . y) \/ (B . y) is set
((I,A,B) \/ B) . y is set
I is set

A /\ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
B . B is set
A . B is set
{(B . B)} is non empty finite set
(A . B) /\ {(B . B)} is finite set
(I,B) . B is finite set
(A . B) /\ ((I,B) . B) is finite set
(A /\ (I,B)) . B is set
I is set

B /\ (I,A) is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
B . B is set
(B /\ (I,A)) . B is set
(I,A) . B is finite set
(B . B) /\ ((I,A) . B) is finite set
{(A . B)} is non empty finite set
(B . B) /\ {(A . B)} is finite set
I is set

(I,A,B) /\ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
B . y is set
((I,A,B) /\ B) . y is set
(I,A,B) . y is finite set
((I,A,B) . y) /\ (B . y) is finite set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} /\ (B . y) is finite set
y is set
A . y is set
B . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} /\ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) /\ (B . y) is finite set
((I,A,B) /\ B) . y is set
y is set
B . y is set
B . y is set
A . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} /\ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) /\ (B . y) is finite set
((I,A,B) /\ B) . y is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) /\ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(A . B)} /\ (B . B) is finite set
(I,A) . B is finite set
((I,A) . B) /\ (B . B) is finite set
((I,A) /\ B) . B is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A,B) /\ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(A . y),(B . y)} /\ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) /\ (B . y) is finite set
((I,A,B) /\ B) . y is set
y is set
X is set
A . X is set
B . X is set
{(A . X),(B . X)} is non empty finite set
B . X is set
{(A . X),(B . X)} /\ (B . X) is finite set
y is set
A . y is set
B . y is set
y is set
X is set
A . X is set
B . X is set
{(A . X),(B . X)} is non empty finite set
B . X is set
{(A . X),(B . X)} /\ (B . X) is finite set
y is set
B . y is set
B . y is set
I is set

B \ (I,B) is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
(B \ (I,B)) . y is set
(I,B) . y is finite set
(B . y) \ ((I,B) . y) is set
B . y is set
{(B . y)} is non empty finite set
(B . y) \ {(B . y)} is set
I is set

B \ (I,B) is Relation-like I -defined Function-like V14(I) set
y is set
X is set
A . X is set
(B \ (I,B)) . X is set
B . X is set
(I,B) . X is finite set
(B . X) \ ((I,B) . X) is set
B . X is set
{(B . X)} is non empty finite set
(B . X) \ {(B . X)} is set
X is set
A . X is set
B . X is set
I is set

A \ (I,B) is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
B . B is set
{(B . B)} is non empty finite set
(A . B) \ {(B . B)} is set
(I,B) . B is finite set
(A . B) \ ((I,B) . B) is set
B is set
y is set
A . y is set
B . y is set
{(B . y)} is non empty finite set
(A . y) \ {(B . y)} is set
B is set
B . B is set
A . B is set
I is set

(I,A) \ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
{(A . B)} is non empty finite set
B . B is set
{(A . B)} \ (B . B) is finite set
(I,A) . B is finite set
((I,A) . B) \ (B . B) is finite set
((I,A) \ B) . B is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A) \ B is Relation-like I -defined Function-like V14(I) set
B is set
A . B is set
B . B is set
{(A . B)} is non empty finite set
{(A . B)} \ (B . B) is finite set
(I,A) . B is finite set
((I,A) . B) \ (B . B) is finite set
((I,A) \ B) . B is set
B is set
A . B is set
B . B is set
((I,A) \ B) . B is set
(I,A) . B is finite set
((I,A) . B) \ (B . B) is finite set
{(A . B)} is non empty finite set
{(A . B)} \ (B . B) is finite set
() . B is set
I is set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(A . y),(B . y)} \ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
((I,A,B) \ B) . y is set
{(A . y)} is non empty finite set
I is set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(A . y),(B . y)} \ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
((I,A,B) \ B) . y is set
A . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
B . y is set
{(A . y),(B . y)} \ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
((I,A,B) \ B) . y is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
B . y is set
B . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
((I,A,B) \ B) . y is set
y is set
B . y is set
B . y is set
A . y is set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \ (B . y) is finite set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
((I,A,B) \ B) . y is set
y is set
A . y is set
B . y is set
B . y is set
((I,A,B) \ B) . y is set
(I,A,B) . y is finite set
((I,A,B) . y) \ (B . y) is finite set
{(A . y),(B . y)} is non empty finite set
{(A . y),(B . y)} \ (B . y) is finite set
() . y is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

A \ (I,B,B) is Relation-like I -defined Function-like V14(I) set
y is set
A . y is set
(A \ (I,B,B)) . y is set
(I,B,B) . y is finite set
(A . y) \ ((I,B,B) . y) is set
() . y is set
A . y is set
B . y is set
{(B . y)} is non empty finite set
(A \ (I,B,B)) . y is set
(I,B,B) . y is finite set
(A . y) \ ((I,B,B) . y) is set
B . y is set
{(B . y),(B . y)} is non empty finite set
(A . y) \ {(B . y),(B . y)} is set
() . y is set
A . y is set
B . y is set
{(B . y)} is non empty finite set
(A \ (I,B,B)) . y is set
(I,B,B) . y is finite set
(A . y) \ ((I,B,B) . y) is set
B . y is set
{(B . y),(B . y)} is non empty finite set
(A . y) \ {(B . y),(B . y)} is set
() . y is set
A . y is set
B . y is set
B . y is set
{(B . y),(B . y)} is non empty finite set
(A \ (I,B,B)) . y is set
(I,B,B) . y is finite set
(A . y) \ ((I,B,B) . y) is set
(A . y) \ {(B . y),(B . y)} is set
() . y is set
I is set

is non empty finite V29() set
[:I,:] is set
bool [:I,:] is set

B is set
A . B is set
[|A,B|] . B is set
B . B is set
[:(A . B),(B . B):] is set
() . B is set
B is set
B . B is set
[|A,B|] . B is set
A . B is set
[:(A . B),(B . B):] is set
() . B is set
I is set

B is set
A . B is set
B . B is set
[:(A . B),(B . B):] is set
[|A,B|] . B is set
[:(B . B),(A . B):] is set
I is set

B is set
A . B is set
[:(A . B),(A . B):] is set
[|A,A|] . B is set
B . B is set
[:(B . B),(B . B):] is set
I is set

y is set
B . y is set
B . y is set
A . y is set
[|B,A|] . y is set
[|B,A|] . y is set
[:(B . y),(A . y):] is set
[:(B . y),(A . y):] is set
y is set
B . y is set
B . y is set
A . y is set
[|A,B|] . y is set
[|A,B|] . y is set
[:(A . y),(B . y):] is set
[:(A . y),(B . y):] is set
I is set

y is set
[|A,B|] . y is set
[|B,B|] . y is set
A . y is set
B . y is set
B . y is set
[:(A . y),(B . y):] is set
[:(B . y),(B . y):] is set
y is set
[|B,A|] . y is set
[|B,B|] . y is set
A . y is set
B . y is set
B . y is set
[:(B . y),(A . y):] is set
[:(B . y),(B . y):] is set
I is set

X is set
[|A,B|] . X is set
[|B,y|] . X is set
A . X is set
B . X is set
B . X is set
y . X is set
[:(A . X),(B . X):] is set
[:(B . X),(y . X):] is set
I is set

[|(A \/ B),B|] is Relation-like I -defined Function-like V14(I) set

[|B,(A \/ B)|] is Relation-like I -defined Function-like V14(I) set

y is set
[|(A \/ B),B|] . y is set
(A \/ B) . y is set
B . y is set
[:((A \/ B) . y),(B . y):] is set
A . y is set
B . y is set
(A . y) \/ (B . y) is set
[:((A . y) \/ (B . y)),(B . y):] is set
[:(A . y),(B . y):] is set
[:(B . y),(B . y):] is set
[:(A . y),(B . y):] \/ [:(B . y),(B . y):] is set
[|A,B|] . y is set
([|A,B|] . y) \/ [:(B . y),(B . y):] is set
[|B,B|] . y is set
([|A,B|] . y) \/ ([|B,B|] . y) is set
([|A,B|] \/ [|B,B|]) . y is set
y is set
[|B,(A \/ B)|] . y is set
B . y is set
(A \/ B) . y is set
[:(B . y),((A \/ B) . y):] is set
A . y is set
B . y is set
(A . y) \/ (B . y) is set
[:(B . y),((A . y) \/ (B . y)):] is set
[:(B . y),(A . y):] is set
[:(B . y),(B . y):] is set
[:(B . y),(A . y):] \/ [:(B . y),(B . y):] is set
[|B,A|] . y is set
([|B,A|] . y) \/ [:(B . y),(B . y):] is set
[|B,B|] . y is set
([|B,A|] . y) \/ ([|B,B|] . y) is set
([|B,A|] \/ [|B,B|]) . y is set
I is set

[|(A \/ B),(B \/ y)|] is Relation-like I -defined Function-like V14(I) set

([|A,B|] \/ [|A,y|]) \/ [|B,B|] is Relation-like I -defined Function-like V14(I) set

(([|A,B|] \/ [|A,y|]) \/ [|B,B|]) \/ [|B,y|] is Relation-like I -defined Function-like V14(I) set
X is set
[|(A \/ B),(B \/ y)|] . X is set
(A \/ B) . X is set
(B \/ y) . X is set
[:((A \/ B) . X),((B \/ y) . X):] is set
A . X is set
B . X is set
(A . X) \/ (B . X) is set
[:((A . X) \/ (B . X)),((B \/ y) . X):] is set
B . X is set
y . X is set
(B . X) \/ (y . X) is set
[:((A . X) \/ (B . X)),((B . X) \/ (y . X)):] is set
[:(A . X),(B . X):] is set
[:(A . X),(y . X):] is set
[:(A . X),(B . X):] \/ [:(A . X),(y . X):] is set
[:(B . X),(B . X):] is set
([:(A . X),(B . X):] \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):] is set
[:(B . X),(y . X):] is set
(([:(A . X),(B . X):] \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set
[|A,B|] . X is set
([|A,B|] . X) \/ [:(A . X),(y . X):] is set
(([|A,B|] . X) \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):] is set
((([|A,B|] . X) \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set
[|A,y|] . X is set
([|A,B|] . X) \/ ([|A,y|] . X) is set
(([|A,B|] . X) \/ ([|A,y|] . X)) \/ [:(B . X),(B . X):] is set
((([|A,B|] . X) \/ ([|A,y|] . X)) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set
[|B,B|] . X is set
(([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X) is set
((([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X)) \/ [:(B . X),(y . X):] is set
[|B,y|] . X is set
((([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X)) \/ ([|B,y|] . X) is